{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:24:04Z","timestamp":1750307044397,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,4,22]],"date-time":"2015-04-22T00:00:00Z","timestamp":1429660800000},"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":["ACM SIGLOG News"],"published-print":{"date-parts":[[2015,4,22]]},"abstract":"<jats:p>\n            Turing in his seminal paper \"Checking a Large Routine\" [Turing 1949] already asked the question whether it was possible to check a routine was\n            <jats:italic>right<\/jats:italic>\n            . Among other contributions, he proposed flowcharts as a concise program representation. He also described a method based on the insight that a programmer should make a number of definite assertions which can be proven individually, and from which the correctness of the whole program could easily follow. It took several years until Floyd [Floyd 1967] and Hoare [Hoare 1969], inspired by McCarthy [McCarthy 1963] and Naur [Naur 1966]'s works, established a logic based on a deductive system what is called today\n            <jats:italic>Floyd-Hoare logic<\/jats:italic>\n            that allowed proving correctness of programs in a rigorous manner. Dijkstra [Dijkstra 1975] presented the first semi-algorithmic view of the Floyd-Hoare logic based on the ideas of\n            <jats:italic>predicate transformers<\/jats:italic>\n            . Since then, the field of software verification has been growing rapidly during the last decades with many available techniques. Among them,\n            <jats:italic>Abstract Interpretation<\/jats:italic>\n            [Cousot and Cousot 1977],\n            <jats:italic>Model Checking<\/jats:italic>\n            [Clarke and Emerson 1981; Queille and Sifakis 1982], and\n            <jats:italic>Symbolic Execution<\/jats:italic>\n            [King 1976] are probably the most predominant algorithmic (i.e., fully automated) techniques today.\n          <\/jats:p>","DOI":"10.1145\/2766189.2766195","type":"journal-article","created":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T22:26:16Z","timestamp":1585952776000},"page":"29-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Algorithmic logic-based verification"],"prefix":"10.1145","volume":"2","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[{"name":"SEI\/CMU"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[{"name":"NASA Ames\/CMU"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[{"name":"NASA Ames\/SGT"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,4,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_21"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_52"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer. 2015. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). In TACAS.  Dirk Beyer. 2015. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). In TACAS .","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer Alessandro Cimatti Alberto Griggio M. Erkan Keremoglu and Roberto Sebastiani. 2009. Software model checking via large-block encoding. In FMCAD. 25--32.  Dirk Beyer Alessandro Cimatti Alberto Griggio M. Erkan Keremoglu and Roberto Sebastiani. 2009. Software model checking via large-block encoding. In FMCAD . 25--32.","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220881.3220981"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In CAV. 184--190.   Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In CAV . 184--190.","DOI":"10.1007\/978-3-642-22110-1_16"},{"volume-title":"VMCAI","year":"2015","author":"Bj\u00f8rner Nikolaj","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","unstructured":"Nikolaj Bj\u00f8rner Kenneth L. McMillan and Andrey Rybalchenko. 2012. Program Verification as Satisfiability Modulo Theories. In SMT. 3--11.  Nikolaj Bj\u00f8rner Kenneth L. McMillan and Andrey Rybalchenko. 2012. Program Verification as Satisfiability Modulo Theories. In SMT . 3--11."},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Kenneth L. McMillan and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS. 105--125.  Nikolaj Bj\u00f8rner Kenneth L. McMillan and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS . 105--125.","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_4"},{"volume-title":"IKOS: A Framework for Static Analysis Based on Abstract Interpretation. In SEFM. 271--277.","year":"2014","author":"Brat Guillaume","key":"e_1_2_1_12_1"},{"volume-title":"Proceedings of the 1987 Symposium on Logic Programming","year":"1987","author":"Bruynooghe Maurice","key":"e_1_2_1_13_1"},{"volume-title":"Workshop","year":"1981","author":"Clarke Edmund M.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi and Maurizio Proietti. 2014. VeriMAP: A Tool for Verifying Programs through Transformations. In TACAS. 568--574.  Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi and Maurizio Proietti. 2014. VeriMAP: A Tool for Verifying Programs through Transformations. In TACAS . 568--574.","DOI":"10.1007\/978-3-642-54862-8_47"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Giorgio Delzanno and Andreas Podelski. 1999. Model Checking in CLP. In TACAS. 223--239.   Giorgio Delzanno and Andreas Podelski. 1999. Model Checking in CLP. In TACAS . 223--239.","DOI":"10.1007\/3-540-49059-0_16"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan. 2003. Automatic Software Model Checking Using CLP. In ESOP. 189--203.   Cormac Flanagan. 2003. Automatic Software Model Checking Using CLP. In ESOP . 189--203.","DOI":"10.1007\/3-540-36575-3_14"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_21_1","first-page":"4","article-title":"Failure tabled constraint logic programming by interpolation","volume":"13","author":"Gange Graeme","year":"2013","journal-title":"TPLP"},{"volume-title":"5th International Symposium, NFM","year":"2013","author":"Garoche Pierre-Lo\u00efc","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"volume-title":"CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings. 412--417","year":"2011","author":"Gupta Ashutosh","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0162-x"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Arie Gurfinkel Sagar Chaki and Samir Sapra. 2011. Efficient Predicate Abstraction of Program Summaries. In NFM. 131--145.   Arie Gurfinkel Sagar Chaki and Samir Sapra. 2011. Efficient Predicate Abstraction of Program Summaries. In NFM . 131--145.","DOI":"10.1007\/978-3-642-20398-5_11"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Arie Gurfinkel Temesghen Kahsai and Jorge A. Navas. 2015. SeaHorn: A Framework For Verifying C Programs - (Competition Contribution). In To appear in TACAS.  Arie Gurfinkel Temesghen Kahsai and Jorge A. Navas. 2015. SeaHorn: A Framework For Verifying C Programs - (Competition Contribution). In To appear in TACAS .","DOI":"10.1007\/978-3-662-46681-0_41"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_9"},{"key":"e_1_2_1_29_1","unstructured":"Kim S. Henriksen and John P. Gallagher. 2006. CHA: Convex Hull Analyser for constraint logic programs. (2006).  Kim S. Henriksen and John P. Gallagher. 2006. CHA: Convex Hull Analyser for constraint logic programs. (2006)."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Manuel V. Hermenegildo Germ\u00e1n Puebla Francisco Bueno and Pedro L\u00f3pez-Garc\u00eda. 2003. Program Development Using Abstract Interpretation (And The Ciao System Preprocessor). In SAS. 127--152.   Manuel V. Hermenegildo Germ\u00e1n Puebla Francisco Bueno and Pedro L\u00f3pez-Garc\u00eda. 2003. Program Development Using Abstract Interpretation (And The Ciao System Preprocessor). In SAS . 127--152.","DOI":"10.1007\/3-540-44898-5_8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41635"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2004.5"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Anvesh Komuravelli Arie Gurfinkel Sagar Chaki and Edmund M. Clarke. 2013. Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In CAV. 846--862.  Anvesh Komuravelli Arie Gurfinkel Sagar Chaki and Edmund M. Clarke. 2013. Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In CAV . 846--862.","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"e_1_2_1_40_1","unstructured":"Akash Lal and Shaz Qadeer. 2014. A program transformation for faster goal-directed search. In FMCAD. 147--154.   Akash Lal and Shaz Qadeer. 2014. A program transformation for faster goal-directed search. In FMCAD . 147--154."},{"key":"e_1_2_1_41_1","unstructured":"Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In CGO. 75--88.   Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In CGO . 75--88."},{"key":"e_1_2_1_42_1","unstructured":"Kim. Marriott and Peter. J. Stuckey. 1998. Introduction to Constraint Logic Programming. MIT Press Cambridge MA USA.   Kim. Marriott and Peter. J. Stuckey. 1998. Introduction to Constraint Logic Programming . MIT Press Cambridge MA USA."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"John McCarthy. 1963. A Basis for a Mathematical Theory of Computation. (1963) 33--70.  John McCarthy. 1963. A Basis for a Mathematical Theory of Computation. (1963) 33--70.","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Mario M\u00e9ndez-Lojo Jorge A. Navas and Manuel V. Hermenegildo. 2007. A Flexible (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In LOPSTR. 154--168.  Mario M\u00e9ndez-Lojo Jorge A. Navas and Manuel V. Hermenegildo. 2007. A Flexible (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In LOPSTR . 154--168.","DOI":"10.1007\/978-3-540-78769-3_11"},{"volume-title":"Proceedings of the North American Conference. 166--185","author":"Muthukumar Kalyan","key":"e_1_2_1_46_1"},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Peter Naur. 1966. Proof of algorithms by general snapshots. 6 (1966) 310--316. Issue 4.  Peter Naur. 1966. Proof of algorithms by general snapshots. 6 (1966) 310--316. Issue 4.","DOI":"10.1007\/BF01966091"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Julio C. Peralta John P. Gallagher and H\u00fcseyin Saglam. 1998. Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In SAS. 246--261.   Julio C. Peralta John P. Gallagher and H\u00fcseyin Saglam. 1998. Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In SAS . 246--261.","DOI":"10.1007\/3-540-49727-7_15"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Philipp R\u00fcmmer Hossein Hojjat and Viktor Kuncak. 2013. Disjunctive Interpolants for Horn-Clause Verification. In CAV. 347--363.  Philipp R\u00fcmmer Hossein Hojjat and Viktor Kuncak. 2013. Disjunctive Interpolants for Horn-Clause Verification. In CAV . 347--363.","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Harald S\u00f8ndergaard. 1986. An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction. In ESOP. 327--338.   Harald S\u00f8ndergaard. 1986. An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction. In ESOP . 327--338.","DOI":"10.1007\/3-540-16442-1_25"},{"key":"e_1_2_1_52_1","unstructured":"Alan Turing. 1949. Checking a Large Routine. (1949).  Alan Turing. 1949. Checking a Large Routine. (1949)."},{"key":"e_1_2_1_53_1","unstructured":"Richard Warren Manuel V. Hermenegildo and Saumya K. Debray. 1988. On the Practicality of Global Flow Analysis of Logic Programs. In ICLP. 684--699.  Richard Warren Manuel V. Hermenegildo and Saumya K. Debray. 1988. On the Practicality of Global Flow Analysis of Logic Programs. In ICLP . 684--699."}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2766189.2766195","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2766189.2766195","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:20:58Z","timestamp":1750238458000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2766189.2766195"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,22]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4,22]]}},"alternative-id":["10.1145\/2766189.2766195"],"URL":"https:\/\/doi.org\/10.1145\/2766189.2766195","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2015,4,22]]},"assertion":[{"value":"2015-04-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}