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...

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard
• Keywords: Automated Reasoning, BAPA Constraints, BAPA Formulas, CADE 2005, Multisorted Theory Bapa