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

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Mon Jul 20 21:57:22 2009 +0200

Added PerezRS09.

---

 htdocs/Documentation/ppl_citations.bib |   40 ++++++++++++++++++++++++++++++++
 1 files changed, 40 insertions(+), 0 deletions(-)

diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib
index 52b0992..03983e9 100644
--- a/htdocs/Documentation/ppl_citations.bib
+++ b/htdocs/Documentation/ppl_citations.bib
@@ -1971,6 +1971,46 @@
               analyser."
 }
 
+ at Inproceedings{PerezRS09,
+  Author = "J. A. {Navarro P{\'e}rez} and A. Rybalchenko and A. Singh",
+  Title = "Cardinality Abstraction for Declarative Networking Applications",
+  Booktitle = "Computer Aided Verification,
+               Proceedings of the 21st International Conference (CAV 2009)",
+  Address = "Grenoble, France",
+  Editor = "A. Bouajjani and O. Maler",
+  Publisher = "Springer",
+  Series = "Lecture Notes in Computer Science",
+  Volume = 5643,
+  Pages = "584--598",
+  Year = 2009,
+  ISBN = "978-3-642-02657-7",
+  Abstract = "Declarative Networking is a recent, viable approach to
+              make distributed programming easier, which is becoming
+              increasingly popular in systems and networking
+              community. It offers the programmer a declarative,
+              rule-based language, called P2, for writing distributed
+              applications in an abstract, yet expressive way. This
+              approach, however, imposes new challenges on analysis
+              and verification methods when they are applied to P2
+              programs. Reasoning about P2 computations is beyond the
+              scope of existing tools since it requires handling of
+              program states defined in terms of collections of
+              relations, which store the application data, together
+              with multisets of tuples, which represent communication
+              events in-flight. In this paper, we propose a
+              cardinality abstraction technique that can be used to
+              analyze and verify P2 programs. It keeps track of the
+              size of relations (together with projections thereof)
+              and multisets defining P2 states, and provides an
+              appropriate treatment of declarative operations, e.g.,
+              indexing, unification, variable binding, and
+              negation. Our cardinality abstraction-based verifier
+              successfully proves critical safety properties of a P2
+              implementation of the Byzantine fault tolerance protocol
+              Zyzzyva, which is a representative and complex
+              declarative networking application."
+}
+
 @Techreport{Pop06,
   Author = "S. Pop and G.-A. Silber and A. Cohen and C. Bastoul
             and S. Girbal and N. Vasilache",