{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:35Z","timestamp":1773193535850,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":55,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540280057","type":"print"},{"value":"9783540318644","type":"electronic"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_20","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"260-277","source":"Crossref","is-referenced-by-count":33,"title":["An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huu Hai","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North Holland, Amsterdam (1954)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1007\/3-540-52885-7_120","volume-title":"10th International Conference on Automated Deduction","author":"P.B. Andrews","year":"1990","unstructured":"Andrews, P.B., Issar, S., Nesmith, D., Pfenning, F.: The TPS theorem proving system. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 641\u2013642. Springer, Heidelberg (1990)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-30482-1_32","volume-title":"Formal Methods and Software Engineering","author":"K. Arkoudas","year":"2004","unstructured":"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.\u00a03308, pp. 373\u2013390. Springer, Heidelberg (2004)"},{"key":"20_CR4","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.(ed.): The Description Logic Handbook: Theory, Implementation and Applications. In: CUP (2003)"},{"key":"20_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-540-31982-5_27","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Bozga","year":"2005","unstructured":"Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 425\u2013439. Springer, Heidelberg (2005)"},{"key":"20_CR7","doi-asserted-by":"crossref","first-page":"191","DOI":"10.36045\/bbms\/1103408547","volume":"1","author":"V. Bruy\u00e9re","year":"1994","unstructured":"Bruy\u00e9re, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin\u00a01, 191\u2013238 (1994)","journal-title":"Bull. Belg. Math. Soc. Simon Stevin"},{"key":"20_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing","author":"D. Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing. Springer, Heidelberg (2001)"},{"key":"20_CR9","unstructured":"Chaieb, A., Nipkow, T.: Generic proof synthesis for Presburger arithmetic. Technical report, Technische Universit\u00e4t M\u00fcnchen (October 2003)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Chin, W.-N., Khoo, S.-C., Xu, D.N.: Extending sized types with with collection analysis. In: ACM PEPM 2003 (2003)","DOI":"10.1145\/777388.777397"},{"key":"20_CR11","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 91\u2013100. Edinburgh University Press (1972)"},{"key":"20_CR12","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories Palo Alto (2003)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Dewar, R.K.: Programming by refinement, as exemplified by the SETL representation sublanguage. In: ACM TOPLAS (July 1979)","DOI":"10.1145\/357062.357064"},{"key":"20_CR14","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S. Feferman","year":"1959","unstructured":"Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundamenta Mathematicae\u00a047, 57\u2013103 (1959)","journal-title":"Fundamenta Mathematicae"},{"key":"20_CR15","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"J. Ferrante","year":"1979","unstructured":"Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol.\u00a0718. Springer, Heidelberg (1979)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"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.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"20_CR17","volume-title":"Introduction to HOL, a theorem proving environment for higher-order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL, a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)"},{"issue":"10","key":"20_CR18","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"20_CR19","volume-title":"Encyclopedia of Mathematics and its Applications","author":"W. Hodges","year":"1993","unstructured":"Hodges, W.: Model Theory. In: Encyclopedia of Mathematics and its Applications, vol.\u00a042, Cambridge University Press, Cambridge (1993)"},{"key":"20_CR20","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: IMACS Intl. Conf. on Applications of Computer Algebra (2004)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N. Klarlund","year":"2000","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, p. 182. Springer, Heidelberg (2000)"},{"key":"20_CR22","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(80)90048-1","volume":"10","author":"D. Kozen","year":"1980","unstructured":"Kozen, D.: Complexity of boolean algebras. Theoretical Computer Science\u00a010, 221\u2013247 (1980)","journal-title":"Theoretical Computer Science"},{"key":"20_CR23","unstructured":"Kuncak, V.: The Jahob project web page (2004), http:\/\/www.mit.edu\/~vkuncak\/projects\/jahob\/"},{"key":"20_CR24","unstructured":"Kuncak, V., Rinard, M.: On the theory of structural subtyping. Technical Report 879, Laboratory for Computer Science, Massachusetts Institute of Technology (2003)"},{"key":"20_CR25","unstructured":"Kuncak, V., Rinard, M.: Structural subtyping of non-recursive types is decidable. In: Eighteenth Annual IEEE Symposium on Logic in Computer Science (2003)"},{"key":"20_CR26","unstructured":"Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (July 2004)"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages, AIOOL 2005 (2005)","DOI":"10.1016\/j.entcs.2005.01.022"},{"key":"20_CR28","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/981009.981016","volume":"39","author":"P. Lam","year":"2004","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Notices\u00a039, 46\u201355 (2004)","journal-title":"SIGPLAN Notices"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"20_CR30","unstructured":"LASH. The LASH Toolset, http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"20_CR31","first-page":"228","volume":"76","author":"L. Loewenheim","year":"1915","unstructured":"Loewenheim, L.: \u00dcber m\u00f6gligkeiten im relativkalk\u00fcl. Math. Annalen\u00a076, 228\u2013251 (1915)","journal-title":"Math. Annalen"},{"key":"20_CR32","unstructured":"Marriott, K., Odersky, M.: Negative boolean constraints. Technical Report 94\/203, Monash University (August 1994)"},{"issue":"3","key":"20_CR33","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0747-7171(89)80013-6","volume":"7","author":"U. Martin","year":"1989","unstructured":"Martin, U., Nipkow, T.: Boolean unification: The story so far. Journal of Symbolic Computation\u00a07(3), 275\u2013293 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378851"},{"issue":"2","key":"20_CR35","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"20_CR38","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: ACM POPL (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"20_CR39","unstructured":"Presburger, M.: \u00fcber die vollst\u00e4ndigkeit eines gewissen systems der aritmethik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Comptes Rendus du premier Congr\u00e8s des Math\u00e9maticiens des Pays slaves, Warsawa, pp. 92\u2013101 (1929)"},{"key":"20_CR40","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/125826.125848","volume-title":"Supercomputing 1991: Proceedings of the 1991 ACM\/IEEE conference on Supercomputing","author":"W. Pugh","year":"1991","unstructured":"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\u201313. ACM Press, New York (1991)"},{"key":"20_CR41","first-page":"320","volume-title":"ACM STOC","author":"C.R. Reddy","year":"1978","unstructured":"Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, pp. 320\u2013325. ACM Press, New York (1978)"},{"key":"20_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30204-9_1","volume-title":"Advances in Databases and Information Systems","author":"P. Revesz","year":"2004","unstructured":"Revesz, P.: Quantifier-elimination for the first-order theory of boolean algebras with linear cardinality constraints. In: Bencz\u00far, A.A., Demetrovics, J., Gottlob, G. (eds.) ADBIS 2004. LNCS, vol.\u00a03255, pp. 1\u201321. Springer, Heidelberg (2004)"},{"key":"20_CR43","unstructured":"Ruess, H., Shankar, N.: Deconstructing Shostak. In: Proc. 16th IEEE LICS (2001)"},{"key":"20_CR44","doi-asserted-by":"crossref","unstructured":"Rugina, R.: Quantitative shape analysis. In: Static Analysis Symposium, SAS 2004 (2004)","DOI":"10.1007\/978-3-540-27864-1_18"},{"issue":"3","key":"20_CR45","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"20_CR46","unstructured":"Skolem, T.: Untersuchungen \u00fcber die Axiome des Klassenkalk\u00fcls and \u00fcber Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen. Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, Oslo, vol. 3 (1919)"},{"key":"20_CR47","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: 14th International Conference on Computer-Aided Verification (2002)","DOI":"10.1007\/3-540-45657-0_40"},{"key":"20_CR48","volume-title":"Handbook of Formal Languages Vol.3: Beyond Words","author":"W. Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages Vol.3: Beyond Words, Springer, Heidelberg (1997)"},{"key":"20_CR49","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.: Combining non-stably infinite theories. Journal of Automated Reasoning (2004) (Accepted for publication)","DOI":"10.1007\/s10817-005-5204-9"},{"key":"20_CR50","unstructured":"Tiwari, A.: Decision procedures in automated deduction. PhD thesis, Department of Computer Science, State University of New York at Stony Brook (2000)"},{"issue":"2","key":"20_CR51","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of Vampire (implementing bottom-up procedures with code trees). Journal of Automated Reasoning\u00a015(2), 237\u2013265 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR52","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: 10th TACAS (2004)","DOI":"10.1007\/978-3-540-24730-2_39"},{"key":"20_CR53","unstructured":"Zarba, C.G.: The Combination Problem in Automated Reasoning. PhD thesis, Stanford University (2004)"},{"key":"20_CR54","series-title":"Lecture Notes in Computer Science","first-page":"762","volume-title":"Verification: Theory and Practice","author":"C.G. Zarba","year":"2004","unstructured":"Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 762\u2013782. Springer, Heidelberg (2004)"},{"key":"20_CR55","unstructured":"Zarba, C.G.: A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In: 18th International Workshop on Unification (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:46:58Z","timestamp":1635727618000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/11532231_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}