{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:04Z","timestamp":1763468224036,"version":"3.28.0"},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987603","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"115-122","source":"Crossref","is-referenced-by-count":7,"title":["Small inductive safe invariants"],"prefix":"10.1109","author":[{"given":"Alexander","family":"Ivrii","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Belov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"17","article-title":"Computer aided verification-25th international conference","volume":"8044","author":"sharygina","year":"2013","journal-title":"CAV"},{"journal-title":"Hardware Model Checking Competition","year":"2013","key":"15"},{"key":"16","first-page":"2011","article-title":"International conference on formal methods in computer-Aided design","volume":"11","author":"bjesse","year":"2011","journal-title":"FMCAD"},{"key":"13","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1007\/11564751_73","article-title":"Towards an optimal cnf encoding of boolean cardinality constraints","volume":"3709","author":"sinz","year":"2005","journal-title":"CP ser Lecture Notes in Computer Science"},{"journal-title":"Hardware Model Checking Competition","year":"2011","key":"14"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"12","first-page":"135","article-title":"Incremental formal verification of hardware","author":"chockler","year":"2011","journal-title":"FMCAD"},{"key":"3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","article-title":"Interpolation and sat-based model checking","volume":"2725","author":"mcmillan","year":"2003","journal-title":"CAV Ser Lecture Notes in Computer Science"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.16"},{"key":"1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","article-title":"Automatic abstraction without counterexamples","volume":"2619","author":"mcmillan","year":"2003","journal-title":"TACAS Ser Lecture Notes in Computer Science"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_7"},{"key":"7","first-page":"123","article-title":"Muser2: An efficient mus extractor","volume":"8","author":"belov","year":"2012","journal-title":"JSAT"},{"key":"6","first-page":"144","article-title":"An incremental approach to model checking progress properties","author":"bradley","year":"2011","journal-title":"FMCAD"},{"key":"5","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"e\ufffdn","year":"2011","journal-title":"FMCAD"},{"key":"4","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"Sat-based model checking without unrolling","volume":"6538","author":"bradley","year":"2011","journal-title":"VMCAI Ser Lecture Notes in Computer Science"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679410"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_39"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2014,10,21]]},"location":"Lausanne, Switzerland","end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987603.pdf?arnumber=6987603","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T02:54:05Z","timestamp":1498186445000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987603\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987603","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}