{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:43:31Z","timestamp":1725770611723},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.23919\/fmcad.2017.8102251","type":"proceedings-article","created":{"date-parts":[[2017,11,9]],"date-time":"2017-11-09T21:49:00Z","timestamp":1510264140000},"page":"132-139","source":"Crossref","is-referenced-by-count":13,"title":["Property directed reachability with word-level abstraction"],"prefix":"10.23919","author":[{"given":"Yen-Sheng","family":"Ho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2016.7427999"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886662"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.21236\/ADA470547"},{"journal-title":"Ebmc The enhanced bounded model checker","year":"0","author":"kroening","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_56"},{"key":"ref15","article-title":"A toolbox for counter-example analysis and optimization","author":"mishchenko","year":"0","journal-title":"Proc of IWLS'13"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.286"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"ref18","article-title":"Lazy abstraction and sat-based reachability in Hardware model checking","author":"vizel","year":"0","journal-title":"Proc of FMCAD'12"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378260"},{"key":"ref4","article-title":"Learning conditional abstractions","author":"brady","year":"0","journal-title":"Proc of FMCAD’ 11"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558624"},{"key":"ref8","article-title":"Efficient implementation of property directed reachability","author":"e\u00e9n","year":"0","journal-title":"Proc FMCAD'11"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214874"},{"journal-title":"Symbolic Model Checking Without BDDs","year":"0","author":"biere","key":"ref2"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_25"},{"key":"ref9","article-title":"An extensible sat-solver","author":"e\u00e9n","year":"0","journal-title":"Proceedings of SAT '03"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2014.6742978"},{"key":"ref21","article-title":"QF BV model checking with property directed reachability","author":"welp","year":"0","journal-title":"Proc of DATE’10"}],"event":{"name":"2017 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2017,10,2]]},"location":"Vienna","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\/08102251.pdf?arnumber=8102251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T22:41:12Z","timestamp":1513032072000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8102251\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":21,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2017.8102251","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}