{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T07:07:48Z","timestamp":1777360068517,"version":"3.51.4"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.23919\/fmcad.2017.8102238","type":"proceedings-article","created":{"date-parts":[[2017,11,9]],"date-time":"2017-11-09T16:49:00Z","timestamp":1510246140000},"page":"31-38","source":"Crossref","is-referenced-by-count":17,"title":["Efficient generation of all minimal inductive validity cores"],"prefix":"10.23919","author":[{"given":"Elaheh","family":"Ghassabani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"ref31","doi-asserted-by":"crossref","DOI":"10.1109\/5.97300","article-title":"The synchronous dataflow programming language Lustre","author":"halbwachs","year":"1991","journal-title":"Proceedings of the IEEE"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-013-9146-2"},{"key":"ref34","year":"0","journal-title":"All IVCs repository"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115632"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886669"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987603"},{"key":"ref13","year":"2016","journal-title":"Center of Excellence for Software Traceability"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ICRE.2003.1232745"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2007.195"},{"key":"ref16","article-title":"From MaxSAT to MinUNSAT: Insights and applications","author":"liffiton","year":"2005","journal-title":"Ann Arbor"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_5"},{"key":"ref18","article-title":"Muser2: An efficient mus extractor","author":"belov","year":"2012","journal-title":"JSAT Journal"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.288"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref4","article-title":"Integration of formal analysis into a model-based software development process","author":"whalen","year":"2007","journal-title":"FMICS"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_20"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"ref6","year":"0","journal-title":"Cadence JasperGold Formal Verification Platform"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.41"},{"key":"ref8","article-title":"Extracting small unsatisfiable cores from unsatisfiable boolean formula","author":"zhang","year":"0","journal-title":"SAT '03"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950346"},{"key":"ref2","article-title":"Checking safety properties using induction and a SAT-solver","author":"sheeran","year":"2000","journal-title":"FMCAD '02"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2016.35"},{"key":"ref1","article-title":"Efficient implementation of property directed reachability","author":"een","year":"0","journal-title":"FMCAD'11"},{"key":"ref20","doi-asserted-by":"crossref","DOI":"10.3233\/AIC-2012-0523","article-title":"Towards efficient MUS extraction","author":"belov","year":"2012","journal-title":"AI communications"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-015-9183-0"},{"key":"ref21","article-title":"Accelerated deletion-based extraction of minimal unsatisfiable cores","author":"nadel","year":"2014","journal-title":"JSAT Journal"},{"key":"ref24","article-title":"Deviation analysis via model checking","author":"heimdahl","year":"2002","journal-title":"ASE 02"},{"key":"ref23","author":"hanna","year":"2015","journal-title":"Formal verification coverage metrics for circuit design properties"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_35"},{"key":"ref25","year":"0","journal-title":"JKind"}],"event":{"name":"2017 Formal Methods in Computer-Aided Design (FMCAD)","location":"Vienna","start":{"date-parts":[[2017,10,2]]},"end":{"date-parts":[[2017,10,6]]}},"container-title":["2017 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8093672\/8102222\/08102238.pdf?arnumber=8102238","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T09:53:08Z","timestamp":1603273988000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8102238\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":34,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2017.8102238","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}