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

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

+@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",