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 sets, and supports a...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30488 |
| _version_ | 1826216150742073344 |
|---|---|
| author | Kuncak, Viktor Nguyen, Huu Hai Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Kuncak, Viktor Nguyen, Huu Hai Rinard, Martin |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | 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 sets, and supports arbitrary quantification over both 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 annotations contain quantifiers themselves, or when proving simulation relation conditions for refinement and equivalence of program fragments. Furthermore, BAPA constraints can be used to extend the techniques for proving the termination of integer programs to 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 the satisfiability and validity problems for 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 though 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. |
| first_indexed | 2024-09-23T16:43:05Z |
| id | mit-1721.1/30488 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:43:05Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304882019-04-11T06:23:33Z An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic Kuncak, Viktor Nguyen, Huu Hai Rinard, Martin Computer Architecture 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 sets, and supports arbitrary quantification over both 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 annotations contain quantifiers themselves, or when proving simulation relation conditions for refinement and equivalence of program fragments. Furthermore, BAPA constraints can be used to extend the techniques for proving the termination of integer programs to 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 the satisfiability and validity problems for 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 though 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. 2005-12-22T01:35:58Z 2005-12-22T01:35:58Z 2004-07-19 MIT-CSAIL-TR-2004-049 MIT-LCS-TR-958 http://hdl.handle.net/1721.1/30488 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 26 p. 26003902 bytes 1120584 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Kuncak, Viktor Nguyen, Huu Hai Rinard, Martin An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic |
| title | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic |
| title_full | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic |
| title_fullStr | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic |
| title_full_unstemmed | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic |
| title_short | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic |
| title_sort | algorithm for deciding bapa boolean algebra with presburger arithmetic |
| url | http://hdl.handle.net/1721.1/30488 |
| work_keys_str_mv | AT kuncakviktor analgorithmfordecidingbapabooleanalgebrawithpresburgerarithmetic AT nguyenhuuhai analgorithmfordecidingbapabooleanalgebrawithpresburgerarithmetic AT rinardmartin analgorithmfordecidingbapabooleanalgebrawithpresburgerarithmetic AT kuncakviktor algorithmfordecidingbapabooleanalgebrawithpresburgerarithmetic AT nguyenhuuhai algorithmfordecidingbapabooleanalgebrawithpresburgerarithmetic AT rinardmartin algorithmfordecidingbapabooleanalgebrawithpresburgerarithmetic |