Sciweavers

Share
CADE
2005
Springer

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic

10 years 12 months ago
An Algorithm for Deciding BAPA: 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 a priory unbounded finite sets, and supports arbitrary quantification over sets and integers. Our 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 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
Comments (0)
books