{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:47:52Z","timestamp":1770288472722,"version":"3.49.0"},"reference-count":20,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,9]]},"DOI":"10.1109\/fmcad.2015.7542257","type":"proceedings-article","created":{"date-parts":[[2016,8,15]],"date-time":"2016-08-15T20:28:56Z","timestamp":1471292936000},"page":"89-96","source":"Crossref","is-referenced-by-count":34,"title":["Compositional verification of procedural programs using horn clauses over integers and arrays"],"prefix":"10.1109","author":[{"given":"Anvesh","family":"Komuravelli","sequence":"first","affiliation":[]},{"given":"Nikolaj","family":"Bjorner","sequence":"additional","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Kenneth L.","family":"Mcmillan","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","article-title":"Ultimate Automizer with SMTlnterpol - (Competition Contribution)","year":"2013","journal-title":"TACAS"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_21"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_41"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"ref18","article-title":"Solving Constrained Horn Clauses using Interpolation","author":"mcmillan","year":"2013","journal-title":"Tech Rep MSR-TR-2013-6"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_51"},{"key":"ref4","article-title":"Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015)","author":"beyer","year":"2015","journal-title":"TACAS"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"ref6","article-title":"SAT-Based Model Checking without Unrolling","author":"bradley","year":"2011","journal-title":"VMCAI"},{"key":"ref5","article-title":"Program Verification as Satisfiability Modulo Theories","author":"bjorner","year":"2012","journal-title":"SMT"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"ref1","author":"ackermann","year":"1954","journal-title":"Solvable Cases of the Decision Problem"},{"key":"ref9","article-title":"Efficient Implementation of Property Directed Reachability","author":"een","year":"2011","journal-title":"FMCAD"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932480"}],"event":{"name":"2015 Formal Methods in Computer-Aided Design (FMCAD)","location":"Austin, TX, USA","start":{"date-parts":[[2015,9,27]]},"end":{"date-parts":[[2015,9,30]]}},"container-title":["2015 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7539356\/7542233\/07542257.pdf?arnumber=7542257","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,17]],"date-time":"2017-03-17T20:55:47Z","timestamp":1489784147000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7542257\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2015.7542257","relation":{},"subject":[],"published":{"date-parts":[[2015,9]]}}}