{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:05:31Z","timestamp":1768907131421,"version":"3.49.0"},"reference-count":22,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987617","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"219-226","source":"Crossref","is-referenced-by-count":22,"title":["Predicate abstraction for reactive synthesis"],"prefix":"10.1109","author":[{"given":"Adam","family":"Walker","sequence":"first","affiliation":[]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"User-guided device driver synthesis","author":"ryzhyk","year":"2014","journal-title":"OSDI"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987617"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"16","first-page":"364","author":"piterman","year":"2006","journal-title":"Synthesis of Reactive 1) Designs"},{"key":"13","first-page":"72","article-title":"Construction of abstract state graphs with pvs","author":"graf","year":"1997","journal-title":"CAV"},{"key":"14","first-page":"886","article-title":"Counterexample-guided control","author":"henzinger","year":"2003","journal-title":"ICALP"},{"key":"11","article-title":"Abstraction refinement for games with incomplete information","author":"dimitrova","year":"2008","journal-title":"FSTTCS"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33365-1_9"},{"key":"21","year":"0","journal-title":"Termite 2 Driver Synthesis Tool"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"20","first-page":"275","article-title":"A game-based framework for ctl counterexamples and 3-valued abstraction-refinement","author":"shoham","year":"2003","journal-title":"CAV"},{"key":"2","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1145\/277044.277186","article-title":"A decision procedure for bit-vector arithmetic","author":"barrett","year":"1998","journal-title":"Proceedings 1998 Design and Automation Conference 35th DAC (Cat No 98CH36175) DAC"},{"key":"1","first-page":"388","article-title":"Refining approximations in software predicate abstraction","author":"ball","year":"2004","journal-title":"TACAS"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_6"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"6","first-page":"154","article-title":"Counterexampleguided abstraction refinement","author":"clarke","year":"2000","journal-title":"CAV"},{"key":"5","first-page":"90","article-title":"Automatic synthesis of robust and optimal controllers-An industrial case study","author":"cassez","year":"2009","journal-title":"HSCC"},{"key":"4","first-page":"49","author":"burch","year":"1991","journal-title":"Symbolic Model Checking with Partitioned Transition Relations"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319611"},{"key":"8","first-page":"51","article-title":"Successive approximation of abstract transition relations","author":"das","year":"2001","journal-title":"LICS"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","location":"Lausanne, Switzerland","start":{"date-parts":[[2014,10,21]]},"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\/06987617.pdf?arnumber=6987617","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\/6987617\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":22,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987617","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}