{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T12:33:11Z","timestamp":1726057991679},"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":28,"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":[{"journal-title":"TACAS","article-title":"Ultimate Automizer with SMTlnterpol - (Competition Contribution)","year":"2013","key":"ref10"},{"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"},{"journal-title":"Tech Rep MSR-TR-2013-6","article-title":"Solving Constrained Horn Clauses using Interpolation","year":"2013","author":"mcmillan","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_51"},{"journal-title":"TACAS","article-title":"Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015)","year":"2015","author":"beyer","key":"ref4"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"journal-title":"VMCAI","article-title":"SAT-Based Model Checking without Unrolling","year":"2011","author":"bradley","key":"ref6"},{"journal-title":"SMT","article-title":"Program Verification as Satisfiability Modulo Theories","year":"2012","author":"bjorner","key":"ref5"},{"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"},{"journal-title":"Solvable Cases of the Decision Problem","year":"1954","author":"ackermann","key":"ref1"},{"journal-title":"FMCAD","article-title":"Efficient Implementation of Property Directed Reachability","year":"2011","author":"een","key":"ref9"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932480"}],"event":{"name":"2015 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2015,9,27]]},"location":"Austin, TX, USA","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":"http:\/\/dx.doi.org\/10.1109\/fmcad.2015.7542257","relation":{},"subject":[],"published":{"date-parts":[[2015,9]]}}}
