Module: ppl/w3ppl Branch: master Commit: 5b1155a6c45815f9ff288374ec00a23016169309 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=5b1155a6c45...
Author: Roberto Bagnara bagnara@cs.unipr.it Date: Fri Apr 16 14:40:41 2010 +0200
Added BandaG10.
---
htdocs/Documentation/ppl_citations.bib | 27 +++++++++++++++++++++++++++ 1 files changed, 27 insertions(+), 0 deletions(-)
diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index e51ce00..8cc053d 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -1365,6 +1365,33 @@ procedure." }
+@Inproceedings{BandaG10, + Author = "G. Banda and J. P. Gallagher", + Title = "Constraint-Based Abstraction of a Model Checker + for Infinite State Systems", + Booktitle = "Proceedings of the 23rd Workshop on (Constraint) + Logic Programming (WLP 2009)", + Editor = "U. Geske and A. Wolf", + Address = "Potsdam, Germany", + Publisher = "Potsdam Universit{"a}tsverlag", + Year = 2010, + Pages = "109--124", + Abstract = "Abstract interpretation-based model checking provides an + approach to verifying properties of infinite-state + systems. In practice, most previous work on abstract + model checking is either restricted to verifying + universal properties, or develops special techniques for + temporal logics such as modal transition systems or + other dual transition systems. By contrast we apply + completely standard techniques for constructing abstract + interpretations to the abstraction of a CTL semantic + function, without restricting the kind of properties + that can be verified. Furthermore we show that this + leads directly to implementation of abstract model + checking algorithms for abstract domains based on + constraints, making use of an SMT solver." +} + @Inproceedings{GulavaniR06, Author = "B. S. Gulavani and S. K. Rajamani", Title = "Counterexample Driven Refinement for Abstract Interpretation",