{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:41:51Z","timestamp":1761964911209,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106307","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"487-497","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Craig vs. Newton in software model checking"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Dietsch","sequence":"first","affiliation":[{"name":"University of Freiburg, Germany"}]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}]},{"given":"Betim","family":"Musa","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}]},{"given":"Alexander","family":"Nutz","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_21"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_3_2_1_3_1","volume-title":"McMillan","author":"Albarghouthi Aws","year":"2013","unstructured":"Aws Albarghouthi and Kenneth L . McMillan . 2013 . Beautiful Interpolants. In CAV (Lecture Notes in Computer Science), Vol. 8044 . Springer , 313\u2013329. Aws Albarghouthi and Kenneth L. McMillan. 2013. Beautiful Interpolants. In CAV (Lecture Notes in Computer Science), Vol. 8044. Springer, 313\u2013329."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV","author":"Barrett Clark","year":"2011","unstructured":"Clark Barrett , Christopher L Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovi\u0107 , Tim King , Andrew Reynolds , and Cesare Tinelli . 2011 . CVC4 . In CAV 2011. Springer, 171\u2013177. Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In CAV 2011. Springer, 171\u2013177."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250769"},{"key":"e_1_3_2_1_10_1","first-page":"184","article-title":"CPAchecker","volume":"2011","author":"Beyer Dirk","year":"2011","unstructured":"Dirk Beyer and M. Erkan Keremoglu . 2011 . CPAchecker : A Tool for Configurable Software Verification. In CAV 2011. 184 \u2013 190 . Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In CAV 2011. 184\u2013190.","journal-title":"A Tool for Configurable Software Verification. In CAV"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"e_1_3_2_1_12_1","volume-title":"FORTE","author":"Beyer Dirk","year":"2015","unstructured":"Dirk Beyer , Stefan L\u00f6we , and Philipp Wendler . 2015 . Sliced Path Prefixes: An Effective Method to Enable Refinement Selection . In FORTE 2015. 228\u2013243. Dirk Beyer, Stefan L\u00f6we, and Philipp Wendler. 2015. Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. In FORTE 2015. 228\u2013243."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"volume-title":"SAS (Lecture Notes in Computer Science)","author":"Brain Martin","key":"e_1_3_2_1_14_1","unstructured":"Martin Brain , Vijay D\u2019Silva , Alberto Griggio , Leopold Haller , and Daniel Kroening . 2013. Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL . In SAS (Lecture Notes in Computer Science) , Vol. 7935 . Springer , 412\u2013432. Martin Brain, Vijay D\u2019Silva, Alberto Griggio, Leopold Haller, and Daniel Kroening. 2013. Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. In SAS (Lecture Notes in Computer Science), Vol. 7935. Springer, 412\u2013432."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9237-y"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_39"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9365-5"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_24_1","first-page":"271","article-title":"SLAB","volume":"2010","author":"Dr\u00e4ger Klaus","year":"2010","unstructured":"Klaus Dr\u00e4ger , Andrey Kupriyanov , Bernd Finkbeiner , and Heike Wehrheim . 2010 . SLAB : A Certifying Model Checker for Infinite-State Concurrent Systems. In TACAS 2010. 271 \u2013 274 . Klaus Dr\u00e4ger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. 2010. SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. In TACAS 2010. 271\u2013274.","journal-title":"A Certifying Model Checker for Infinite-State Concurrent Systems. In TACAS"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_13"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_41"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_41"},{"volume-title":"Effective word-level interpolation for software verification","author":"Griggio Alberto","key":"e_1_3_2_1_28_1","unstructured":"Alberto Griggio . 2011. Effective word-level interpolation for software verification . In FMCAD. FMCAD Inc ., 28\u201336. Alberto Griggio. 2011. Effective word-level interpolation for software verification. In FMCAD. FMCAD Inc., 28\u201336."},{"key":"e_1_3_2_1_29_1","volume-title":"Thi Thieu Hoa Le, and Roberto Sebastiani","author":"Griggio Alberto","year":"2011","unstructured":"Alberto Griggio , Thi Thieu Hoa Le, and Roberto Sebastiani . 2011 . Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. In TACAS (Lecture Notes in Computer Science), Vol. 6605 . Springer , 143\u2013157. Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani. 2011. Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. In TACAS (Lecture Notes in Computer Science), Vol. 6605. Springer, 143\u2013157."},{"key":"e_1_3_2_1_30_1","volume-title":"Automatically Refining Abstract Interpretations. In TACAS","author":"Gulavani Bhargav S.","year":"2008","unstructured":"Bhargav S. Gulavani , Supratik Chakraborty , Aditya V. Nori , and Sriram K. Rajamani . 2008 . Automatically Refining Abstract Interpretations. In TACAS 2008 . Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, and Sriram K. Rajamani. 2008. Automatically Refining Abstract Interpretations. In TACAS 2008."},{"key":"e_1_3_2_1_31_1","unstructured":"443\u2013458.  443\u2013458."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_34"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_68"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706353"},{"key":"e_1_3_2_1_36_1","unstructured":"1706353  1706353"},{"key":"e_1_3_2_1_37_1","volume-title":"Software Model Checking for People Who Love Automata. In CAV","author":"Heizmann Matthias","year":"2013","unstructured":"Matthias Heizmann , Jochen Hoenicke , and Andreas Podelski . 2013 . Software Model Checking for People Who Love Automata. In CAV 2013. 36\u201352. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013. Software Model Checking for People Who Love Automata. In CAV 2013. 36\u201352."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_40_1","unstructured":"503279  503279"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065016"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_1_44_1","unstructured":"Springer 459\u2013473.  Springer 459\u2013473."},{"volume-title":"CAV (1) (Lecture Notes in Computer Science)","author":"Karbyshev Aleksandr","key":"e_1_3_2_1_45_1","unstructured":"Aleksandr Karbyshev , Nikolaj Bj\u00f8rner , Shachar Itzhaky , Noam Rinetzky , and Sharon Shoham . 2015. Property-Directed Inference of Universal Invariants or Proving Their Absence . In CAV (1) (Lecture Notes in Computer Science) , Vol. 9206 . Aleksandr Karbyshev, Nikolaj Bj\u00f8rner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham. 2015. Property-Directed Inference of Universal Invariants or Proving Their Absence. In CAV (1) (Lecture Notes in Computer Science), Vol. 9206."},{"key":"e_1_3_2_1_46_1","unstructured":"Springer 583\u2013602.  Springer 583\u2013602."},{"key":"e_1_3_2_1_47_1","volume-title":"This is Boogie 2. Manuscript Working Draft. (24 jun","author":"Leino K. Rustan M.","year":"2008","unstructured":"K. Rustan M. Leino . 2008. This is Boogie 2. Manuscript Working Draft. (24 jun 2008 ). Microsoft Research , Redmond, WA, USA (http:\/\/research.microsoft.com\/ en-us\/um\/people\/leino\/papers\/krml178.pdf). K. Rustan M. Leino. 2008. This is Boogie 2. Manuscript Working Draft. (24 jun 2008). Microsoft Research, Redmond, WA, USA (http:\/\/research.microsoft.com\/ en-us\/um\/people\/leino\/papers\/krml178.pdf)."},{"volume-title":"CAV (Lecture Notes in Computer Science)","author":"McMillan Kenneth L.","key":"e_1_3_2_1_48_1","unstructured":"Kenneth L. McMillan . 2003. Interpolation and SAT-Based Model Checking . In CAV (Lecture Notes in Computer Science) , Vol. 2725 . Springer , 1\u201313. Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In CAV (Lecture Notes in Computer Science), Vol. 2725. Springer, 1\u201313."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_1_51_1","volume-title":"FMCAD","author":"McMillan Kenneth L.","year":"2011","unstructured":"Kenneth L. McMillan . 2011 . Interpolants from Z3 Proofs . In FMCAD 2011. 19\u201327. http:\/\/dl.acm.org\/citation.cfm?id=2157661 Kenneth L. McMillan. 2011. Interpolants from Z3 Proofs. In FMCAD 2011. 19\u201327. http:\/\/dl.acm.org\/citation.cfm?id=2157661"},{"key":"e_1_3_2_1_52_1","volume-title":"Automatic Abstraction Without Counterexamples. In TACAS","author":"Kenneth","year":"2003","unstructured":"Kenneth L. McMillan and Nina Amla. 2003 . Automatic Abstraction Without Counterexamples. In TACAS 2003 . 2\u201317. Kenneth L. McMillan and Nina Amla. 2003. Automatic Abstraction Without Counterexamples. In TACAS 2003. 2\u201317."},{"key":"e_1_3_2_1_53_1","volume-title":"Kurshan","author":"Namjoshi Kedar S.","year":"2000","unstructured":"Kedar S. Namjoshi and Robert P . Kurshan . 2000 . Syntactic Program Transformations for Automatic Abstraction. In CAV (Lecture Notes in Computer Science), Vol. 1855 . Springer , 435\u2013449. Kedar S. Namjoshi and Robert P. Kurshan. 2000. Syntactic Program Transformations for Automatic Abstraction. In CAV (Lecture Notes in Computer Science), Vol. 1855. Springer, 435\u2013449."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_44"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.06.005"}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Paderborn Germany","acronym":"ESEC\/FSE'17"},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106307","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106307","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:37Z","timestamp":1750217437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106307"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":54,"alternative-id":["10.1145\/3106237.3106307","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106307","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}