The Interval Sharing Tree Data Structure

The IST library is a C library that provides a set of functions together with the IST data structure to manipulate interval constraints (i.e. contraints of the form

a <= x <= b

where `a` is a natural number and `b` is a natural number of +infinity

in a multi-dimensional space. More precisely, the sets that can be represented by IST are the sets that can be defined by formulas constructed from the following grammar

phi := x in [a,b] | phi /\ phi | not(phi)

where boolean connectors have the usual semantics. IST is an extension of the CST Covering Sharing Trees) [DR00,DRV04] data structure based on the Sharing Tree data structure [Zam97]. CST allows to represent the sets that can be defined by formulas constructed from the following grammar

 phi := x in [a,+infty] | phi /\ phi | phi \/ phi

Additionally to the traditional operations on sets [GMD+07,Gan02], some useful operations for the verification of discrete systems have been implemented [Van03, Gan02, DRV02]. An example of discrete systems which are handled by the library are models obtained by applying a so-called counting abstraction on abstractions of multi-threaded Java programs. The verification problem that is solved using the library is the coverability problem (a mild form of the reachability problem). We developed some coverability checking tools. More information is given in the section about coverability checkers.

References

[GMD+07] Pierre Ganty, Cédric Meuter, Giorgio Delzanno, Gabriel Kalyon, Jean-François Raskin, Laurent Van Begin. Symbolic Data Structure for sets of k-uples. Technical Report 570, Université Libre de Bruxelles, 2007.

[GVanb04] Pierre Ganty, Laurent Van Begin. Non Deterministic Automata for the Efficient Representation of Infinite-state Systems. Proceedings of CP+CV, 1st workshop on Constraint Programming and Constraints for Verification, Barcelona, Spain, 2004.

[DRV04] Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. CSTs (Covering Sharing Trees): compact Data Structures for Parameterized Verification. Will appear in Software Tools for Technology Transfer manuscript, 2004.

[Gan02] Pierre Ganty. Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles. Master's Thesis, Université Libre de Bruxelles, Bruxelles, Belgium, 2002.

[DR00] Giorgio Delzanno and Jean-François Raskin. Symbolic Representation of Upward-Closed Sets. In the proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'00), Lecture Notes in Computer Science 1785, pages 426--440, Springer, 2000.

[Zam97] Denis Zampuniéris. The Sharing Tree data structure: Theory and Applications in Formal Verification. Ph.D. Thesis, Facultés Universitaires Notre-Dame de la Paix, Namur, Belgium.