{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T06:37:52Z","timestamp":1781764672653,"version":"3.54.5"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2012,12,1]],"date-time":"2012-12-01T00:00:00Z","timestamp":1354320000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CMACS"],"award-info":[{"award-number":["CMACS"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2012,12]]},"abstract":"<jats:p>The algebraic\/model theoretic design of static analyzers uses abstract domains based on representations of properties and pre-calculated property transformers. It is very efficient. The logical\/proof theoretic approach uses SMT solvers\/theorem provers and computation of property transformers on-the-fly. It is very expressive. We propose to unify both approaches, so that they can be combined to reach the sweet spot best adapted to a specific application domain in the precision\/cost spectrum. We first give a new formalization of the proof theoretic approach in the abstract interpretation framework, introducing a semantics based on multiple interpretations to deal with the soundness of such approaches. Then we describe how to combine them with any other abstract interpretation-based analysis using an iterated reduction to combine abstractions. The key observation is that the Nelson-Oppen procedure, which decides satisfiability in a combination of logical theories by exchanging equalities and disequalities, computes a reduced product (after the state is enhanced with some new \u201cobservations\u201d corresponding to alien terms). By abandoning restrictions ensuring completeness (such as disjointness, convexity, stably-infiniteness, or shininess, etc.), we can even broaden the application scope of logical abstractions for static analysis (which is incomplete anyway).<\/jats:p>","DOI":"10.1145\/2395116.2395120","type":"journal-article","created":{"date-parts":[[2013,1,8]],"date-time":"2013-01-08T15:34:16Z","timestamp":1357659256000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Theories, solvers and static analysis by abstract interpretation"],"prefix":"10.1145","volume":"59","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[{"name":"Courant Institute of Mathematical Sciences, New York University and \u00c9cole Normale Sup\u00e9rieure &amp; Inria, Paris, New York, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[{"name":"\u00c9cole Normale Sup\u00e9rieure &amp; Inria, Paris and Centre National de la Recherche Scientifique, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[{"name":"Instituto Madrile\u00f1o de Estudios Avanzados, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,1,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2010-3385"},{"key":"e_1_2_1_2_1","unstructured":"Bradley A. and Manna Z. 2007. The Calculus of Computation Decision procedures with Applications to Verification. Springer Berlin.   Bradley A. and Manna Z. 2007. The Calculus of Computation Decision procedures with Applications to Verification. Springer Berlin."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_2_1_4_1","volume-title":"Eds.","volume":"73","author":"Chang C."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Chen L. Min\u00e9 A. Wang J. and \n      Cousot P\n  . \n  2011\n  . Linear absolute value relation analysis. In Proceedings of the 20th European Symposium on Programming (ESOP) Saarbr\u00fccken Germany G. Barthe Ed. Lecture Notes in Computer Science Series vol. \n  6602 Springer-Verlag Berlin 156--175.   Chen L. Min\u00e9 A. Wang J. and Cousot P. 2011. Linear absolute value relation analysis. In Proceedings of the 20th European Symposium on Programming (ESOP) Saarbr\u00fccken Germany G. Barthe Ed. Lecture Notes in Computer Science Series vol. 6602 Springer-Verlag Berlin 156--175.","DOI":"10.1007\/978-3-642-19718-5_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_7_1","first-page":"91","article-title":"Theorem proving in arithmetic without multiplication","volume":"91","author":"Cooper D.","year":"1972","journal-title":"Mach. Intell."},{"key":"e_1_2_1_9_1","series-title":"Handbook of Theoretical Computer Science Series","volume-title":"Methods and logics for proving programs","author":"Cousot P."},{"key":"e_1_2_1_10_1","volume-title":"The calculational design of a generic abstract interpreter, invited chapter","author":"Cousot P."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00313-3"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 2nd International Symposium on Programming. 106--130","author":"Cousot P."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_14_1","first-page":"185","article-title":"A constructive characterization of the lattices of all retractions, pre-closure, quasi-closure and closure operators on a complete lattice","volume":"38","author":"Cousot P.","year":"1979","journal-title":"Portug. Math."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Cousot P.\n     and \n      Cousot R\n  . \n  1992\n  b. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (PLILP'92) M. Bruynooghe and M. Wirsing Eds. Lecture Notes in Computer Science vol. \n  631\n  . \n  Springer Berlin 269--295.   Cousot P. and Cousot R. 1992b. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (PLILP'92) M. Bruynooghe and M. Wirsing Eds. Lecture Notes in Computer Science vol. 631. Springer Berlin 269--295.","DOI":"10.1007\/3-540-55844-6_142"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. Monniaux D. and \n      Rival X\n  . \n  2008\n  . Combination of abstractions in the Astr\u00e9e static analyzer. In Proceedings of the 11th Annual Asian Computing Science Conference (ASIAN 06). M. Okada and I. Satoh Eds. Lecture Notes in Computer Scinece vol. \n  4435 Springer Berlin 272--300.   Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. Monniaux D. and Rival X. 2008. Combination of abstractions in the Astr\u00e9e static analyzer. In Proceedings of the 11th Annual Asian Computing Science Conference (ASIAN 06). M. Okada and I. Satoh Eds. Lecture Notes in Computer Scinece vol. 4435 Springer Berlin 272--300.","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Cousot P. Cousot R. and \n      Mauborgne L\n  . \n  2010\n  . A scalable segmented decision tree abstract domain. In Pnueli Festschrift Z. Manna and D. Peled Eds. Lecture Notes in Computer Science vol. \n  6200 Springer-Verlag Berlin 72--95.   Cousot P. Cousot R. and Mauborgne L. 2010. A scalable segmented decision tree abstract domain. In Pnueli Festschrift Z. Manna and D. Peled Eds. Lecture Notes in Computer Science vol. 6200 Springer-Verlag Berlin 72--95.","DOI":"10.1007\/978-3-642-13754-9_5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 15th Computer-Aided Verification Conference (CAV'03)","volume":"2725","author":"de Moura L."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96725"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.005"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90037-8"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1137\/0204006"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449791"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/646250.685678"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Goubault E. Martel M. and \n      Putot S\n  . \n  2002\n  . Asserting the precision of floating-point computations: A simple abstract interpreter. In Proceedings of the 11th European Symposium on Programming (ESOP) D. Le M\u00e9tayer Ed. Lecture Notes in Computer Science Series vol. \n  2305 Springer Berlin 209--212.   Goubault E. Martel M. and Putot S. 2002. Asserting the precision of floating-point computations: A simple abstract interpreter. In Proceedings of the 11th European Symposium on Programming (ESOP) D. Le M\u00e9tayer Ed. Lecture Notes in Computer Science Series vol. 2305 Springer Berlin 209--212.","DOI":"10.1007\/3-540-45927-8_15"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646830.707569"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480912"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_2_1_40_1","unstructured":"Gulwani S.\n     and \n      Necula G. C\n  . \n  2007\n  . Path-sensitive analysis for linear arithmetic and uninterpreted functions. In Proceedings of the 11th International Symposium on Static Analysis (SAS'04) R. Giacobazzi Ed. Lecture Notes in Computer Science Series vol. \n  3148 Springer Berlin 328--343.  Gulwani S. and Necula G. C. 2007. Path-sensitive analysis for linear arithmetic and uninterpreted functions. In Proceedings of the 11 th International Symposium on Static Analysis (SAS'04) R. Giacobazzi Ed. Lecture Notes in Computer Science Series vol. 3148 Springer Berlin 328--343."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134026"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480945.1480960"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00042-1"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), B. Nebel, Ed., Morgan Kaufmann, 624--634","author":"McIlraith S."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734421"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760292"},{"key":"e_1_2_1_48_1","volume-title":"Introduction to Mathematical Logic","author":"Mendelson E.","edition":"4"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134659"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_51_1","volume-title":"Introduction to Set Theory","author":"Monk J. D."},{"key":"e_1_2_1_52_1","first-page":"171","article-title":"L'op\u00e9ration de fermeture et ses invariants dans les syst\u00e8mes partiellement ordonn\u00e9s","volume":"3","author":"Monteiro A.","year":"1942","journal-title":"Portugal. Math."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_54_1","doi-asserted-by":"crossref","volume-title":"A Course in Model Theory: An Introduction to Contemporary Mathematical Logic","author":"Poizat B.","DOI":"10.1007\/978-1-4419-8622-1"},{"key":"e_1_2_1_55_1","unstructured":"Pratt V. 1977. Two easy theories whose combination is hard. Tech. rep. MIT. September 1 boole.stanford. edu\/pub\/sefnp.pdf.  Pratt V. 1977. Two easy theories whose combination is hard. Tech. rep. MIT. September 1 boole.stanford. edu\/pub\/sefnp.pdf."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2801"},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Reps T. Sagiv S. and \n      Yorsh G\n  . \n  2004\n  . Symbolic implementation of the best transformer. In Proceedings of the 5th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI) B. Steffen and G. Levi Eds. Lecture Notes in Computer Notes Science vol. \n  2937 Springer Berlin 252--266.  Reps T. Sagiv S. and Yorsh G. 2004. Symbolic implementation of the best transformer. In Proceedings of the 5th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI) B. Steffen and G. Levi Eds. Lecture Notes in Computer Notes Science vol. 2937 Springer Berlin 252--266.","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the 1st International Workshop on Frontiers of Combining Systems, F. Baader and K. U. Schulz, Eds., Applied Logic. Kluwer Academic Publishers, 103--120","author":"Tinelli C."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-5204-9"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_11"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968865"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2395116.2395120","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2395116.2395120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:56Z","timestamp":1750239296000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2395116.2395120"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12]]},"references-count":62,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["10.1145\/2395116.2395120"],"URL":"https:\/\/doi.org\/10.1145\/2395116.2395120","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,12]]},"assertion":[{"value":"2011-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}