{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T01:56:34Z","timestamp":1789178194501,"version":"build-2803163510"},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,3]]},"DOI":"10.23919\/date.2019.8714819","type":"proceedings-article","created":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T21:29:07Z","timestamp":1558042147000},"page":"456-461","source":"Crossref","is-referenced-by-count":8,"title":["fbPDR: In-depth combination of forward and backward analysis in Property Directed Reachability"],"prefix":"10.23919","author":[{"given":"Tobias","family":"Seufert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","first-page":"517","article-title":"Model checking with multi-threaded ic3 portfolios","author":"chaki","year":"2016","journal-title":"VMCAI"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102254"},{"key":"ref12","first-page":"43","article-title":"Efficient verification of multi-property designs (the benefit of wrong assumptions)","author":"goldberg","year":"2018","journal-title":"DATE"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"ref14","first-page":"31","article-title":"Minimal assignments for bounded model checking","author":"ravi","year":"2004","journal-title":"TACAS"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1126\/science.220.4598.671","article-title":"Optimization by simmulated annealing","volume":"220","author":"kirkpatrick","year":"1983","journal-title":"Science"},{"key":"ref16","article-title":"On the complexity of derivations in propositional calculus","author":"tseitin","year":"1968","journal-title":"Studies in Constructive Mathematics and Mathematical Logics"},{"key":"ref17","first-page":"502","article-title":"An extensible SAT-solver","author":"e\u00e9n","year":"2003","journal-title":"SAT"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8341978"},{"key":"ref3","first-page":"79","article-title":"Sequential verification using Reverse PDR","author":"seufert","year":"2017","journal-title":"MBMV"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_29"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_38"},{"key":"ref2","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"e\u00e9n","year":"2011","journal-title":"FMCAD"},{"key":"ref1","first-page":"70","article-title":"Sat-based model checking without unrolling","author":"bradley","year":"2011","journal-title":"VMCAI"},{"key":"ref9","first-page":"308","article-title":"Intertwined forward-backward reachability analysis using interpolants","author":"vizel","year":"2013","journal-title":"TACAS"}],"event":{"name":"2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)","location":"Florence, Italy","start":{"date-parts":[[2019,3,25]]},"end":{"date-parts":[[2019,3,29]]}},"container-title":["2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8704855\/8714721\/08714819.pdf?arnumber=8714819","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T01:31:32Z","timestamp":1643247092000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8714819\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3]]},"references-count":17,"URL":"https:\/\/doi.org\/10.23919\/date.2019.8714819","relation":{},"subject":[],"published":{"date-parts":[[2019,3]]}}}