{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:41:56Z","timestamp":1743007316055,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_31","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"450-464","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Abstract Interpretation as Automated Deduction"],"prefix":"10.1007","author":[{"given":"Vijay","family":"D\u2019Silva","sequence":"first","affiliation":[]},{"given":"Caterina","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"31_CR1","unstructured":"Abramsky, S.: Domain theory and the logic of observable properties. Ph.D. thesis, University of London (1987)"},{"key":"31_CR2","doi-asserted-by":"publisher","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":"31_CR3","unstructured":"Bj\u00f8rner, N., Duterte, B., de Moura, L.: Accelerating lemma learning using joins - DPLL($$\\sqcup $$). In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR (2008)"},{"issue":"2","key":"31_CR4","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain, M., D\u2019silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45(2), 213\u2013245 (2014)","journal-title":"Formal Methods Syst. Des."},{"key":"31_CR5","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford University Press (1960)"},{"key":"31_CR6","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: POPL, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"issue":"6","key":"31_CR8","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":"31_CR9","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 143\u2013154. ACM Press (2013)","DOI":"10.1145\/2480359.2429087"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) PLDI, pp. 405\u2013416. ACM Press (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"BS Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Schwartzbach, M.I., Ball, T. (eds.) PLDI, pp. 376\u2013386. ACM Press (2006)","DOI":"10.1145\/1133255.1134026"},{"key":"31_CR14","unstructured":"Haller, L.C.R.: Abstract satisfaction. Ph.D. thesis, University of Oxford (2014)"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Hermenegildo, M., Palsberg, J. (eds.) POPL, pp. 71\u201382 (2010)","DOI":"10.1145\/1707801.1706309"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3540543961_17","volume-title":"Functional Programming Languages and Computer Architecture","author":"TP Jensen","year":"1991","unstructured":"Jensen, T.P.: Strictness analysis in logical form. In: Hughes, J. (ed.) Functional Programming Languages and Computer Architecture. LNCS, vol. 523, pp. 352\u2013366. Springer, Heidelberg (1991)"},{"issue":"8","key":"31_CR17","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":"31_CR18","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, pp. 70\u201384. RISC Report 07\u201307 (2007)"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"706","DOI":"10.1007\/978-3-642-23786-7_53","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"M Pelleau","year":"2011","unstructured":"Pelleau, M., Truchet, C., Benhamou, F.: Octagonal domains for continuous constraints. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 706\u2013720. Springer, Heidelberg (2011)"},{"key":"31_CR20","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":"31_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-78163-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"DA Schmidt","year":"2008","unstructured":"Schmidt, D.A.: Internal and external logics of abstract interpretations. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 263\u2013278. Springer, Heidelberg (2008)"},{"key":"31_CR22","unstructured":"Thakur, A.V.: Symbolic abstraction: algorithms and applications. Ph.D. thesis, The University of Wisconsin - Madison (2014)"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Thakur, A.V., Breck, J., Reps, T.W.: Satisfiability modulo abstraction for separation logic with linked lists. In: Rungta, N., Tkachuk, O. (eds.) SPIN, pp. 58\u201367 (2014)","DOI":"10.1145\/2632362.2632376"},{"key":"31_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-33125-1_10","volume-title":"Static Analysis","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 111\u2013128. Springer, Heidelberg (2012)"},{"key":"31_CR25","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2015.02.003","volume":"311","author":"AV Thakur","year":"2015","unstructured":"Thakur, A.V., Lal, A., Lim, J., Reps, T.W.: Posthat and all that: automating abstract interpretation. Electr. Notes Theor. Comput. Sci. 311, 15\u201332 (2015)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"31_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-33125-1_23","volume-title":"Static Analysis","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A Generalization of St\u00e5lmarck\u2019s method. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 334\u2013351. Springer, Heidelberg (2012)"},{"key":"31_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174\u2013192. Springer, Heidelberg (2012)"},{"key":"31_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-73595-3_11","volume-title":"Automated Deduction \u2013 CADE-21","author":"A Tiwari","year":"2007","unstructured":"Tiwari, A., Gulwani, S.: Logical interpretation: static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 147\u2013166. Springer, Heidelberg (2007)"},{"key":"31_CR29","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":"31_CR30","unstructured":"van den Elsen, S.: Weak monadic second-order theory of one successor. Seminar: Decision Procedures (2012)"},{"key":"31_CR31","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T10:42:10Z","timestamp":1676025730000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}