{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T05:54:17Z","timestamp":1648792457621},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,7,27]],"date-time":"2016-07-27T00:00:00Z","timestamp":1469577600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10817-016-9382-4","type":"journal-article","created":{"date-parts":[[2016,7,27]],"date-time":"2016-07-27T12:20:45Z","timestamp":1469622045000},"page":"363-390","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstract Interpretation as Automated Deduction"],"prefix":"10.1007","volume":"58","author":[{"given":"Vijay","family":"D\u2019Silva","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Caterina","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,27]]},"reference":[{"key":"9382_CR1","unstructured":"Abramsky, S.: Domain theory and the logic of observable properties. PhD thesis, University of London (1987)"},{"key":"9382_CR2","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/S0167-6423(99)00007-6","volume":"35","author":"A Aiken","year":"1999","unstructured":"Aiken, A.: Introduction to set constraint-based program analysis. Sci. Comput. Program. 35, 79\u2013111 (1999)","journal-title":"Sci. Comput. Program."},{"key":"9382_CR3","unstructured":"Bj\u00f8rner, N., de\u00a0Moura, L.: Applications of SMT solvers to program verification. In: Notes for the Summer School on Formal Techniques (2014)"},{"key":"9382_CR4","unstructured":"Bj\u00f8rner, N., Duterte, B., de\u00a0Moura, L.: Accelerating lemma learning using joins \u2013 DPLL( $$\\sqcup $$ \u2294 ). In: Proceedings of Logic for Programming, Artificial Intelligence and Reasoning (2008)"},{"key":"9382_CR5","doi-asserted-by":"crossref","unstructured":"Brain, M., D\u2019silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Form. Methods Syst. Des. 45(2), 213\u2013245 (2014)","DOI":"10.1007\/s10703-013-0203-7"},{"key":"9382_CR6","doi-asserted-by":"crossref","unstructured":"Brain, M., Hadarean, L., Kroening, D., Martins, R., Automatic generation of propagation complete SAT encodings. In: Proceedings of Verification, Model Checking and Abstract Interpretation, Springer, pp. 536\u2013556. (2016)","DOI":"10.1007\/978-3-662-49122-5_26"},{"key":"9382_CR7","unstructured":"B\u00fcchi, J. R.: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science, Stanford Univ. Press, pp 1\u201311 (1960)"},{"key":"9382_CR8","unstructured":"Cachera, D., Pichardie, D., Comparing techniques for certified static analysis. In: The NASA Formal Methods Symposium (NFM), NASA Ames Research Center, pp. 111\u2013115. (2009)"},{"key":"9382_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of Principles of Programming Languages, ACM Press, pp. 238\u2013252. (1977)","DOI":"10.1145\/512950.512973"},{"key":"9382_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of Principles of Programming Languages, ACM Press, pp. 269\u2013282. (1979)","DOI":"10.1145\/567752.567778"},{"issue":"6","key":"9382_CR11","first-page":"31:1","volume":"59","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: Theories, solvers and static analysis by abstract interpretation. J. ACM 59(6), 31:1\u201331:56 (2013)","journal-title":"J. ACM"},{"key":"9382_CR12","doi-asserted-by":"crossref","unstructured":"Dalla\u00a0Preda, M., Giacobazzi, R., Lakhotia, A., Mastroeni, I.: Abstract symbolic automata: Mixed syntactic\/semantic similarity analysis of executables. In: Proceedings of Principles of Programming Languages, ACM Press, pp. 329\u2013341. (2015)","DOI":"10.1145\/2676726.2676986"},{"issue":"1","key":"9382_CR13","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/s10703-015-0233-4","volume":"47","author":"L D\u2019antoni","year":"2015","unstructured":"D\u2019antoni, L.: Extended symbolic finite automata and transducers. Form. Methods Syst. Des. 47(1), 93\u2013119 (2015)","journal-title":"Form. Methods Syst. Des."},{"key":"9382_CR14","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Urban, C.: Abstract interpretation as automated deduction. In: Proceedings of Automated Deduction, pp. 450\u2013464. (2015a)","DOI":"10.1007\/978-3-319-21401-6_31"},{"key":"9382_CR15","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Urban, C.: Conflict-driven conditional termination. In: Proceedings of Computer Aided Verification, pp. 471\u2013286. (2015b)","DOI":"10.1007\/978-3-319-21668-3_16"},{"key":"9382_CR16","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Proceedings of Principles of Programming Languages, ACM Press, pp. 143\u2013154. (2013)","DOI":"10.1145\/2429069.2429087"},{"key":"9382_CR17","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract satisfaction. In: Proceedings of Principles of Programming Languages, ACM Press, pp. 139\u2013150. (2014)","DOI":"10.1145\/2535838.2535868"},{"key":"9382_CR18","unstructured":"van\u00a0den Elsen, S.: Weak monadic second-order theory of one successor. Seminar: Decision Procedures, (2012) http:\/\/www.mpi-sws.org\/~piskac\/teaching\/decpro-ws12\/slides\/WS1S.pdf"},{"key":"9382_CR19","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N. P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of Programming Language Design and Implementation, ACM Press, pp. 405\u2013416. (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"9382_CR20","doi-asserted-by":"crossref","unstructured":"Gulavani, B. S., Chakraborty, S., Nori, A. V., Rajamani, S. K.: Automatically refining abstract interpretations. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, Springer, LNCS, vol 4963, pp. 443\u2013458. (2008)","DOI":"10.1007\/978-3-540-78800-3_33"},{"key":"9382_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proceedings of Programming Language Design and Implementation, ACM Press, pp. 376\u2013386. (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"9382_CR22","unstructured":"Haller, L.C.R.: Abstract satisfaction. PhD thesis, University of Oxford (2014)"},{"key":"9382_CR23","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Proceedings of Principles of Programming Languages, pp. 71\u201382. (2010)","DOI":"10.1145\/1706299.1706309"},{"key":"9382_CR24","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proceedings of Computer Aided Verification, Springer, pp. 36\u201352. (2013)","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"9382_CR25","doi-asserted-by":"crossref","unstructured":"Jensen, T. P.: Strictness analysis in logical form. In: FPCA, Springer, pp. 352\u2013366. (1991)","DOI":"10.1007\/3540543961_17"},{"key":"9382_CR26","volume-title":"Stone Spaces. Cambridge Studies in Advanced Mathematics","author":"P Johnstone","year":"1986","unstructured":"Johnstone, P.: Stone Spaces. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge (1986)"},{"key":"9382_CR27","doi-asserted-by":"crossref","unstructured":"Jourdan, J. H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified c static analyzer. In: Proceedings of Principles of Programming Languages, ACM Press, pp. 247\u2013259. (2015)","DOI":"10.1145\/2676726.2676966"},{"issue":"8","key":"9382_CR28","first-page":"89","volume":"4","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Reps, T.W., Seshia, S.A., Thakur, A.V.: Decision procedures and abstract interpretation (Dagstuhl seminar 14351). Dagstuhl Rep. 4(8), 89\u2013106 (2014)","journal-title":"Dagstuhl Rep."},{"key":"9382_CR29","unstructured":"Leino, K.R.M., Logozzo, F.: Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain. In: Workshop on Invariant Generation, RISC Report 07\u201307, pp. 70\u201384. (2007)"},{"key":"9382_CR30","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM 53, 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9382_CR31","doi-asserted-by":"crossref","unstructured":"Pelleau, M., Truchet, C., Benhamou, F.: Octagonal domains for continuous constraints. In: CP, pp. 706\u2013720. (2011)","DOI":"10.1007\/978-3-642-23786-7_53"},{"key":"9382_CR32","volume-title":"The mathematics of metamathematics","author":"H Rasiowa","year":"1963","unstructured":"Rasiowa, H., Sikorski, R.: The mathematics of metamathematics. Polish Academy of Science, Warsaw (1963)"},{"key":"9382_CR33","doi-asserted-by":"crossref","unstructured":"Schmidt, D. A.: Internal and external logics of abstract interpretations. In: Proceedings of Verification, Model Checking and Abstract Interpretation, Springer-Verlag, Berlin, Heidelberg, pp. 263\u2013278. (2008)","DOI":"10.1007\/978-3-540-78163-9_23"},{"key":"9382_CR34","doi-asserted-by":"crossref","unstructured":"Surma, S. J.: On the origin and subsequent applications of the concept of the lindenbaum algebra. In: L\u00a0Jonathan\u00a0Cohen HP Jerzy\u00a0Lo\u015b, Podewski KP (eds) Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Studies in Logic and the Foundations of Mathematics, vol 104, Elsevier, pp. 719\u2013734. (1982)","DOI":"10.1016\/S0049-237X(09)70230-7"},{"key":"9382_CR35","unstructured":"Thakur, A.V: Symbolic abstraction: Algorithms and applications. PhD thesis, The University of Wisconsin\u2014Madison (2014)"},{"key":"9382_CR36","doi-asserted-by":"crossref","unstructured":"Thakur, A.V., Reps, T.: A generalization of St\u00e5lmarck\u2019s method. In: Proceedings of Static Analysis Symposium, Springer (2012a)","DOI":"10.1007\/978-3-642-33125-1_23"},{"key":"9382_CR37","doi-asserted-by":"crossref","unstructured":"Thakur, A.V., Reps, T.W.: A method for symbolic computation of abstract operations. In: Proceedings of Computer Aided Verification (2012b)","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"9382_CR38","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Languages, automata, and logic. In: Rozenberg G, Salomaa A (eds) Handbook of Formal Languages, vol. 3, Springer, pp. 389\u2013455. (1997)","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"9382_CR39","doi-asserted-by":"crossref","unstructured":"Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Proceedings of Automated Deduction, pp. 147\u2013166. (2007)","DOI":"10.1007\/978-3-540-73595-3_11"},{"key":"9382_CR40","doi-asserted-by":"crossref","unstructured":"Truchet, C., Pelleau, M., Benhamou, F.: Abstract domains for constraint programming, with the example of octagons. In: Symbolic and Numeric Algorithms for Scientific Computing, pp. 72\u201379. (2010)","DOI":"10.1109\/SYNASC.2010.69"},{"key":"9382_CR41","unstructured":"Vardi, M. Y., Wilke, T.: Automata: from logics to algorithms. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., pp. 629\u2013736. (2008)"},{"issue":"1","key":"9382_CR42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inform. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inform. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9382-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9382-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9382-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9382-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,11]],"date-time":"2019-09-11T20:05:45Z","timestamp":1568232345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9382-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,27]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["9382"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9382-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7,27]]}}}