[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic

  • Conference paper
Automated Deduction – CADE-20 (CADE 2005)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3632))

Included in the following conference series:

  • 600 Accesses

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.

CADE-20.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Ackermann, W.: Solvable Cases of the Decision Problem. North Holland, Amsterdam (1954)

    MATH  Google Scholar 

  2. Andrews, P.B., Issar, S., Nesmith, D., Pfenning, F.: The TPS theorem proving system. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 641–642. Springer, Heidelberg (1990)

    Google Scholar 

  3. Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a file system implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 373–390. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.(ed.): The Description Logic Handbook: Theory, Implementation and Applications. In: CUP (2003)

    Google Scholar 

  5. Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  6. Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 425–439. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Bruyére, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1, 191–238 (1994)

    MATH  MathSciNet  Google Scholar 

  8. Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  9. Chaieb, A., Nipkow, T.: Generic proof synthesis for Presburger arithmetic. Technical report, Technische Universität München (October 2003)

    Google Scholar 

  10. Chin, W.-N., Khoo, S.-C., Xu, D.N.: Extending sized types with with collection analysis. In: ACM PEPM 2003 (2003)

    Google Scholar 

  11. Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 91–100. Edinburgh University Press (1972)

    Google Scholar 

  12. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories Palo Alto (2003)

    Google Scholar 

  13. Dewar, R.K.: Programming by refinement, as exemplified by the SETL representation sublanguage. In: ACM TOPLAS (July 1979)

    Google Scholar 

  14. Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959)

    MATH  MathSciNet  Google Scholar 

  15. Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer, Heidelberg (1979)

    MATH  Google Scholar 

  16. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Gordon, M.J.C., Melham, T.F.: Introduction to HOL, a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  18. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  19. Hodges, W.: Model Theory. In: Encyclopedia of Mathematics and its Applications, vol. 42, Cambridge University Press, Cambridge (1993)

    Google Scholar 

  20. Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: IMACS Intl. Conf. on Applications of Computer Algebra (2004)

    Google Scholar 

  21. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, p. 182. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. Kozen, D.: Complexity of boolean algebras. Theoretical Computer Science 10, 221–247 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  23. Kuncak, V.: The Jahob project web page (2004), http://www.mit.edu/~vkuncak/projects/jahob/

  24. Kuncak, V., Rinard, M.: On the theory of structural subtyping. Technical Report 879, Laboratory for Computer Science, Massachusetts Institute of Technology (2003)

    Google Scholar 

  25. Kuncak, V., Rinard, M.: Structural subtyping of non-recursive types is decidable. In: Eighteenth Annual IEEE Symposium on Logic in Computer Science (2003)

    Google Scholar 

  26. Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (July 2004)

    Google Scholar 

  27. Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages, AIOOL 2005 (2005)

    Google Scholar 

  28. Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Notices 39, 46–55 (2004)

    Article  Google Scholar 

  29. Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: 6th International Conference on Verification, Model Checking and Abstract Interpretation (2005)

    Google Scholar 

  30. LASH. The LASH Toolset, http://www.montefiore.ulg.ac.be/~boigelot/research/lash/

  31. Loewenheim, L.: Über mögligkeiten im relativkalkül. Math. Annalen 76, 228–251 (1915)

    Google Scholar 

  32. Marriott, K., Odersky, M.: Negative boolean constraints. Technical Report 94/203, Monash University (August 1994)

    Google Scholar 

  33. Martin, U., Nipkow, T.: Boolean unification: The story so far. Journal of Symbolic Computation 7(3), 275–293 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  34. Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)

    Google Scholar 

  35. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  36. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  37. Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  38. Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: ACM POPL (2005)

    Google Scholar 

  39. Presburger, M.: über die vollständigkeit eines gewissen systems der aritmethik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Comptes Rendus du premier Congrès des Mathématiciens des Pays slaves, Warsawa, pp. 92–101 (1929)

    Google Scholar 

  40. Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 1991: Proceedings of the 1991 ACM/IEEE conference on Supercomputing, pp. 4–13. ACM Press, New York (1991)

    Chapter  Google Scholar 

  41. Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, pp. 320–325. ACM Press, New York (1978)

    Google Scholar 

  42. Revesz, P.: Quantifier-elimination for the first-order theory of boolean algebras with linear cardinality constraints. In: Benczúr, A.A., Demetrovics, J., Gottlob, G. (eds.) ADBIS 2004. LNCS, vol. 3255, pp. 1–21. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  43. Ruess, H., Shankar, N.: Deconstructing Shostak. In: Proc. 16th IEEE LICS (2001)

    Google Scholar 

  44. Rugina, R.: Quantitative shape analysis. In: Static Analysis Symposium, SAS 2004 (2004)

    Google Scholar 

  45. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24(3), 217–298 (2002)

    Article  Google Scholar 

  46. Skolem, T.: Untersuchungen über die Axiome des Klassenkalküls and über Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen. Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, Oslo, vol. 3 (1919)

    Google Scholar 

  47. Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: 14th International Conference on Computer-Aided Verification (2002)

    Google Scholar 

  48. Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages Vol.3: Beyond Words, Springer, Heidelberg (1997)

    Google Scholar 

  49. Tinelli, C., Zarba, C.: Combining non-stably infinite theories. Journal of Automated Reasoning (2004) (Accepted for publication)

    Google Scholar 

  50. Tiwari, A.: Decision procedures in automated deduction. PhD thesis, Department of Computer Science, State University of New York at Stony Brook (2000)

    Google Scholar 

  51. Voronkov, A.: The anatomy of Vampire (implementing bottom-up procedures with code trees). Journal of Automated Reasoning 15(2), 237–265 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  52. Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: 10th TACAS (2004)

    Google Scholar 

  53. Zarba, C.G.: The Combination Problem in Automated Reasoning. PhD thesis, Stanford University (2004)

    Google Scholar 

  54. Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 762–782. Springer, Heidelberg (2004)

    Google Scholar 

  55. Zarba, C.G.: A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In: 18th International Workshop on Unification (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT CSAIL, Cambridge, USA

    Viktor Kuncak & Martin Rinard

  2. Singapore-MIT Alliance,  

    Huu Hai Nguyen & Martin Rinard

Authors
  1. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Huu Hai Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Rinard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technical University of Catalonia, Barcelona

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kuncak, V., Nguyen, H.H., Rinard, M. (2005). An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_20

Download citation

  • DOI: https://doi.org/10.1007/11532231_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28005-7

  • Online ISBN: 978-3-540-31864-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation