×

Deciding Boolean algebra with Presburger arithmetic. (English) Zbl 1112.03011

Summary: We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines Boolean algebras of sets of uninterpreted elements (BA) and Presburger arithmetic operations (PA). BAPA can express the relationship between integer variables and cardinalities of unbounded finite sets, and it 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, as well as in constraint database query evaluation and loop invariant inference. We give a formal description of an algorithm for deciding BAPA. We analyze our algorithm and show that it has optimal alternating time complexity and that the complexity of BAPA matches the complexity of PA. 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. When restricted to BA formulas, the algorithm can be used to decide BA in optimal alternating time. Furthermore, the algorithm can eliminate individual quantifiers from a formula with free variables and therefore perform projection onto a desirable set of variables. 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 suggest that a straightforward implementation of the algorithm is effective on nontrivial formulas as long as the number of set variables is small. We also report on a new algorithm for solving the quantifier-free fragment of BAPA.

MSC:

03B35 Mechanization of proofs and logical operations
03B25 Decidability of theories and sets of sentences
68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Ackermann, W.: Solvable Cases of the Decision Problem. North Holland, Amsterdam (1954) · Zbl 0056.24505
[2] Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a file system implementation. In: Sixth International Conference on Formal Engineering Methods (ICFEM ’04), vol. 3308 of LNCS. Seattle (2004)
[3] Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.) The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Boston, Massachusetts (2003) · Zbl 1058.68107
[4] Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification (CAV ’04). Lecture Notes in Computer Science, vol. 3114, pp. 515–518. Boston, Massachusetts (2004) · Zbl 1103.68605
[5] Berman, L.: The complexity of logical theories. Theor. Comp. Sci. 11(1), 71–77 (1980) · Zbl 0475.03017 · doi:10.1016/0304-3975(80)90037-7
[6] Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Logic 6(3), 614–633 (2005) · doi:10.1145/1071596.1071601
[7] Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Berlin Heidelberg New York (1997) · Zbl 0865.03004
[8] Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: FOSSACS’05. Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York (2005) · Zbl 1119.03060
[9] 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) · Zbl 0804.11024
[10] Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Trans. Program. Lang. Syst. 21(4), 747–789 (1999) · Zbl 01935245 · doi:10.1145/325478.325480
[11] Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. J. Autom. Reason. 28(2), 101–142 (2002) · Zbl 1002.68165 · doi:10.1023/A:1015019416843
[12] Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing. Springer, Berlin Heidelberg New York (2001) · Zbl 0981.03056
[13] Chaieb, A., Nipkow, T.: Generic proof synthesis for Presburger arithmetic. Technical report, Technische Universität München (2003) · Zbl 1171.03006
[14] Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28(1), 114–133 (1981) · Zbl 0473.68043
[15] Chin, W.-N., Khoo, S.-C., Xu, D.N.: Extending sized types with collection analysis. In: ACM PEPM’03, San Diego, California (2003)
[16] 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, London, UK (1972) · Zbl 0258.68046
[17] Dewar, R.K.: Programming by refinement, as exemplified by the SETL representation sublanguage. ACM Trans. Program. Lang. Syst. 1(1), 27–49 (1979) · Zbl 0463.68014 · doi:10.1145/357062.357064
[18] Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundam. Math. 47, 57–103 (1959) · Zbl 0088.24803
[19] Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718 Springer, Berlin Heidelberg New York (1979) · Zbl 0404.03028
[20] Gordon, M.J.C., Melham, T.F.: Introduction to HOL, a Theorem Proving Environment for Higher-order Logic. Cambridge University Press, UK (1993) · Zbl 0779.68007
[21] Henriksen, J., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: TACAS ’95. Lecture Notes in Computer Science, vol. 1019. Springer, Berlin Heidelberg New York (1995)
[22] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[23] Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: IMACS International Conference on Applications of Computer Algebra, Beaumont, Texas (2004)
[24] Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Proc. 5th International Conference on Implementation and Application of Automata. Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York (2000) · Zbl 1066.68079
[25] Kozen, D.: Complexity of boolean algebras. Theor. Comput. Sci. 10, 221–247 (1980) · Zbl 0428.03036 · doi:10.1016/0304-3975(80)90048-1
[26] Kozen, D.: Theory of Computation. Springer, Berlin Heidelberg New York (2006) · Zbl 1102.68025
[27] Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: 20th International Conference on Automated Deduction, CADE-20, Tallinn, Estonia (2005) · Zbl 1102.03303
[28] Kuncak, V., Rinard, M.: On the theory of structural subtyping. Technical Report 879. Laboratory for Computer Science, Massachusetts Institute of Technology (2003a) · Zbl 1202.68250
[29] Kuncak, V., Rinard, M.: Structural subtyping of non-recursive types is decidable. In: Eighteenth Annual IEEE Symposium on Logic in Computer Science, Ottawa, Canada (2003b) · Zbl 1067.68054
[30] Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (2004) · Zbl 1202.68250
[31] Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL), Paris, France (2005) · Zbl 1111.68509
[32] Kuncak, V., Rinard, M.: An overview of the Jahob analysis system: Project goals and current status. In: NSF Next Generation Software Workshop, Rhodes, Greece (2006)
[33] Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: CAV’04. Lecture Notes in Computer Science, vol. 3114. Springer, Berlin Heidelberg New York (2004) · Zbl 1103.68628
[34] Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Not. 39, 46–55 (2004) · doi:10.1145/981009.981016
[35] Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: 6th International Conference on Verification, Model Checking and Abstract Interpretation, Paris (2005) · Zbl 1111.68509
[36] Loewenheim, L.: Über Mögligkeiten im Relativkalkül. Math. Ann. 76, 228–251 (1915)
[37] Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (2005) · Zbl 1195.68049
[38] Marriott, K., Odersky, M.: Negative boolean constraints. Technical Report 94/203, Monash University (1994) · Zbl 0872.68017
[39] Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Conference on Programming Language Design and Implementation, Snowbird, Utah (2001)
[40] Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[41] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283 of LNCS. Springer, Berlin Heidelberg New York (2002) · Zbl 0994.68131
[42] Ohlbach, H.J., Koehler, J.: How to extend a formal system with a Boolean algebra component. In: Schmidt, W.B.P.H. (ed.) Automated Deduction. A Basis for Applications, vol. 3, pp. 57–75. Kluwer, Boston, Massachusetts (1998)
[43] Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) 11th CADE, vol. 607 of LNAI, pp. 748–752 (1992)
[44] Papadimitriou, C.H.: On the complexity of integer programming. J. Assoc. Comput. Mach. 28(4), 765–768 (1981) · Zbl 0468.68050
[45] Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: ACM POPL, pp. 132–144. ACM, New York (2005) · Zbl 1369.68152
[46] 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)
[47] Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Supercomputing ’91: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing, Albuquerque, New Mexico, pp. 4–13 (1991)
[48] Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, pp. 320–325. ACM, New York (1978) · Zbl 1282.68142
[49] Revesz, P.: Quantifier-elimination for the first-order theory of boolean algebras with linear cardinality constraints. In: Proc. Advances in Databases and Information Systems (ADBIS’04). Lecture Notes in Computer Science, vol. 3255. Springer, Berlin Heidelberg New York (2004) · Zbl 1110.03016
[50] Ruess, H., Shankar, N.: Deconstructing Shostak. In: Proc. 16th IEEE LICS, Washington–Brussels–New York (2001)
[51] Rugina, R.: Quantitative shape analysis. In: Static Analysis Symposium (SAS’04), Verona, Italy (2004) · Zbl 1104.68422
[52] Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002) · Zbl 05459332 · doi:10.1145/514188.514190
[53] 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, no. 3, Oslo (1919)
[54] Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57–81 (1968) · Zbl 0196.01901 · doi:10.1007/BF01691346
[55] Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages Vol. 3: Beyond Words. Springer, Berlin Heidelberg New York (1997)
[56] Tinelli, C., Zarba, C.: Combining non-stably infinite theories. J. Autom. Reason. 34(3), 209–238 (2005) · Zbl 1108.03014 · doi:10.1007/s10817-005-5204-9
[57] Tiwari, A.: Decision procedures in automated deduction. Ph.D. thesis, Department of Computer Science, State University of New York at Stony Brook (2000)
[58] Voronkov, A.: The anatomy of Vampire (implementing bottom-up procedures with code trees). J. Autom. Reason. 15(2), 237–265 (1995) · Zbl 0838.68100 · doi:10.1007/BF00881918
[59] Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, Chapt. 27, pp. 1965–2013. Elsevier Science, Amsterdam (2001) · Zbl 1011.68129
[60] Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Proceedings of 10th TACAS. Springer, Berlin Heidelberg New York (2004) · Zbl 1126.68359
[61] Zarba, C.G.: The combination problem in automated reasoning. Ph.D. thesis, Stanford University (2004a)
[62] Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772, pp. 762–782. Springer, Berlin Heidelberg New York (2004b) · Zbl 1274.68206
[63] Zarba, C.G.: A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In: 18th International Workshop on Unification (2004c)
[64] Zarba, C.G.: Combining sets with cardinals. J. Autom. Reason. 34(1), 1–29 (2005) · Zbl 1085.03011 · doi:10.1007/s10817-005-3075-8
[65] Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD ’02: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, pp. 442–449. New York, USA (2002)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.