UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Cardinality Abstraction for Declarative Networking Applications

Pérez, JAN; Rybalchenko, A; Singh, A; (2009) Cardinality Abstraction for Declarative Networking Applications. In: Bouajjani, A and Maler, O, (eds.) Computer Aided Verification. 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. (pp. 584 - 598). Springer Berlin Heidelberg Green open access


Download (226kB)


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.

Type: Proceedings paper
Title: Cardinality Abstraction for Declarative Networking Applications
Event: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009
ISBN-13: 978-3-642-02657-7
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-642-02658-4_43
Publisher version: http://dx.doi.org/10.1007/978-3-642-02658-4_43
Language: English
Additional information: This is the authors' accepted version of this published article. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-02658-4_43
URI: http://discovery.ucl.ac.uk/id/eprint/1361359
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item