An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic

paper ps   
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 simulation relation conditions for refinement and equivalence of program fragments. Furthermore, BAPA constraints can be used for proving the termination of programs that manipulate data structures, and have applications in constraint databases. We give a formal description of a decision procedure for BAPA, which implies the decidability of BAPA. We analyze our algorithm and obtain an elementary upper bound on the running time, thereby giving the first complexity bound for BAPA. Because it works by a reduction to PA, our algorithm yields the decidability of a combination of sets of uninterpreted elements with any decidable extension of PA. Our algorithm can also be used to yield an optimal decision procedure for BA through a reduction to PA with bounded quantifiers. We have implemented our algorithm and used it to discharge verification conditions in the Jahob system for data structure consistency checking of Java programs; our experience with the algorithm is promising.

Citation

Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In 20th International Conference on Automated Deduction, CADE-20, volume 3632 of LNCS, Tallinn, Estonia, July 2005. Superseded by [50].

BibTex Entry

@inproceedings{KuncakETAL05AlgorithmDecidingBAPA,
  author = {Viktor Kuncak and Huu Hai Nguyen and Martin Rinard},
  title = {An Algorithm for Deciding {BAPA}: {B}oolean {A}lgebra with {P}resburger {A}rithmetic},
  booktitle = {20th International Conference on Automated Deduction, CADE-20},
  year = 2005,
  address = {Tallinn, Estonia},
  series = {LNCS},
  volume = {3632},
  month = {July},
  note = {Superseded by 
          \cite{KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic}},
  abstract = {
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
simulation relation conditions for refinement and
equivalence of program fragments.  Furthermore, BAPA
constraints can be used for proving the termination of
programs that manipulate data structures, and have
applications in constraint databases.

We give a formal description of a decision procedure for
BAPA, which implies the decidability of BAPA.  We analyze
our algorithm and obtain an elementary upper bound on the
running time, thereby giving the first complexity bound for
BAPA.  Because it works by a reduction to PA, our algorithm
yields the decidability of a combination of sets of
uninterpreted elements with any decidable extension of PA.
Our algorithm can also be used to yield an optimal
decision procedure for BA through a reduction to PA with
bounded quantifiers.

We have implemented our algorithm and used it to discharge
verification conditions in the Jahob system for data
structure consistency checking of Java programs; our
experience with the algorithm is promising.
}
}