{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T14:14:46Z","timestamp":1781014486684,"version":"3.54.1"},"reference-count":32,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007,11]]},"DOI":"10.1109\/iccad.2007.4397277","type":"proceedings-article","created":{"date-parts":[[2008,1,9]],"date-time":"2008-01-09T14:22:47Z","timestamp":1199888567000},"page":"273-280","source":"Crossref","is-referenced-by-count":5,"title":["Computation of minimal counterexamples by using black box techniques and symbolic methods"],"prefix":"10.1109","author":[{"given":"Tobias","family":"Nopper","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref32","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/10722167_13","article-title":"Combining decision diagrams and SAT procedures for efficient symbolic model checking","volume":"1855","author":"williams","year":"2000","journal-title":"Computer Aided Verification"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55179-4_22"},{"key":"ref30","author":"somenzi","year":"2001","journal-title":"CUDD CU decision diagram package release 2 3 1"},{"key":"ref10","article-title":"Symbolic model checking using SAT procedures instead of BDDs","author":"biere","year":"1999","journal-title":"Design Automation Conf"},{"key":"ref11","first-page":"407","article-title":"Checking Safety Properties Using Induction and a SAT-solver","volume":"1954","author":"sheeran","year":"2000","journal-title":"FMCAD"},{"key":"ref12","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":"Computer Aided Verification"},{"key":"ref13","first-page":"31","article-title":"Minimal assignments for bounded model checking","volume":"2988","author":"ravi","year":"2004","journal-title":"TACAS"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_20"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_21"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/43.180261"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.1991.519494"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383966"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.850814"},{"key":"ref28","first-page":"541","article-title":"An extensible sat-solver","volume":"2919","author":"een","year":"2003","journal-title":"Theory and Applications of Satisfiability Testing 6th InternationalConference SAT 2003"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"ref29","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","article-title":"VIS: A system for verification and synthesis","volume":"1102","year":"1996","journal-title":"Computer Aided Verification"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.4"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.841068"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref9","article-title":"Symbolic model checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_20"},{"key":"ref22","article-title":"Flexible modeling of unknowns in model checking for incomplete designs","author":"nopper","year":"2005","journal-title":"ITG\/GI\/GMM- Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-44798-9_23","article-title":"Efficient debugging in a formal verification environment","volume":"2144","author":"copty","year":"2001","journal-title":"Correct Hardware Design and Verification Methods (CHARME)"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-52148-8_30","article-title":"Verification of synchronous sequential machines based on symbolic execution","volume":"407","author":"coudert","year":"1989","journal-title":"Automatic Verification Methods for Finite State Systems"},{"key":"ref23","author":"abramovici","year":"1990","journal-title":"Digital Systems Testing and Testable Design"},{"key":"ref26","doi-asserted-by":"crossref","DOI":"10.1109\/MTV.2006.3","article-title":"Advanced SAT-techniques for bounded model checking of blackbox designs","author":"herbstritt","year":"2006","journal-title":"Proc Microprocessor Test and Verification Workshop (MTV98)"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378471"}],"event":{"name":"2007 IEEE\/ACM International Conference on Computer-Aided Design","location":"San Jose, CA, USA","start":{"date-parts":[[2007,11,4]]},"end":{"date-parts":[[2007,11,8]]}},"container-title":["2007 IEEE\/ACM International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4397222\/4397223\/04397277.pdf?arnumber=4397277","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T14:47:25Z","timestamp":1557154045000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4397277\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/iccad.2007.4397277","relation":{},"ISSN":["1092-3152"],"issn-type":[{"value":"1092-3152","type":"print"}],"subject":[],"published":{"date-parts":[[2007,11]]}}}