Sciweavers

CORR
2004
Springer

The First-Order Theory of Sets with Cardinality Constraints is Decidable

13 years 9 months ago
The First-Order Theory of Sets with Cardinality Constraints is Decidable
Data structures often use an integer variable to keep track of the number of elements they store. An invariant of such data structure is that the value of the integer variable is equal to the number of elements stored in the data structure. Using a program analysis framework ports abstraction of data structures as sets, such constraints can be expressed using the language of sets with cardinality constraints. The same language can be used to express preconditions that guarantee the correct use of the data structure interfaces, and to express invariants useful for the analysis of the termination behavior of programs that manipulate objects stored in data structures. In this paper we show the decidability of valid formulas in one such language. Specifically, we examine the first-order theory that combines 1) Boolean algebras of sets of uninterpreted elements and 2) Presburger arithmetic operations. Our language allows relating the cardinalities of sets to the values of integer variables...
Viktor Kuncak, Martin C. Rinard
Added 17 Dec 2010
Updated 17 Dec 2010
Type Journal
Year 2004
Where CORR
Authors Viktor Kuncak, Martin C. Rinard
Comments (0)