[PPL-devel] [GIT] ppl/w3ppl(master): Added BandaG10.

[Roberto Bagnara]

Module: ppl/w3ppl
Branch: master
Commit: 5b1155a6c45815f9ff288374ec00a23016169309
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=5b1155a6c45815f9ff288374ec00a23016169309

Author: Roberto Bagnara <bagnara at 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."
 }
 
+ at 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",