Sciweavers

JAR
2006

Deciding Boolean Algebra with Presburger Arithmetic

13 years 3 months ago
Deciding Boolean Algebra with Presburger Arithmetic
We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines 1) Boolean algebras of sets of uninterpreted elements (BA) and 2) Presburger arithmetic operations (PA). BAPA can express the relationship between integer variables and cardinalities of unbounded finite sets, and supports arbitrary quantification over sets and integers. Our original motivation for BAPA is deciding verification conditions that arise in the static analysis of data structure consistency properties. Data structures often use an integer variable to keep track of the number of elements they store; an invariant of such a data structure is that the value of the integer variable is equal to the number of elements stored in the data structure. When the data structure content is represented by a set, the resulting constraints can be captured in BAPA. BAPA formulas with quantifier alternations arise when verifying programs with annotations containing quantifiers, or when proving simulatio...
Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JAR
Authors Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
Comments (0)