{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T15:04:12Z","timestamp":1730214252291,"version":"3.28.0"},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1109\/date.2010.5457090","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T13:16:33Z","timestamp":1361279793000},"page":"1707-1712","source":"Crossref","is-referenced-by-count":5,"title":["Tighter integration of BDDs and SMT for Predicate Abstraction"],"prefix":"10.1109","author":[{"given":"A","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"A","family":"Franzen","sequence":"additional","affiliation":[]},{"given":"A","family":"Griggio","sequence":"additional","affiliation":[]},{"given":"K","family":"Kalyanasundaram","sequence":"additional","affiliation":[]},{"given":"M","family":"Roveri","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","first-page":"72","article-title":"Construction of Abstract State Graphs with PVS","volume":"1254","author":"graf","year":"1997","journal-title":"CAV Ser LNCS"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/266021.266068"},{"key":"ref14","first-page":"220","article-title":"Light-Weight Theorem Proving for Debugging and Verifying Units of Code","author":"d\u00e9harbe","year":"2003","journal-title":"SEFM IEEE"},{"key":"ref15","article-title":"Integrating a BDD Prover and a DPLL SAT Solver for Abstract Data Types","author":"schuijers","year":"2006","journal-title":"Tech Univ Eindhoven Tech Rep"},{"key":"ref16","first-page":"299","article-title":"The MathSAT 4SMT Solver","volume":"5123","author":"bruttomesso","year":"2008","journal-title":"CAV Ser LNCS"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"ref4","first-page":"24","article-title":"Predicate abstraction via symbolic decision procedures","volume":"3576","author":"lahiri","year":"2005","journal-title":"CAV Ser LNCS"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_36"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065697"},{"key":"ref5","first-page":"424","article-title":"SMT Techniques for Fast Predicate Abstraction","volume":"4144","author":"lahiri","year":"2006","journal-title":"CAV Ser LNCS"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/FAMCAD.2007.35"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2007.364481"},{"key":"ref2","first-page":"141","article-title":"A Symbolic Approach to Predicate Abstraction","volume":"2725","author":"lahiri","year":"2003","journal-title":"CAV Ser LNCS"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_6"}],"event":{"name":"2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)","start":{"date-parts":[[2010,3,8]]},"location":"Dresden","end":{"date-parts":[[2010,3,12]]}},"container-title":["2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx5\/5450668\/5456897\/05457090.pdf?arnumber=5457090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T22:33:24Z","timestamp":1489876404000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/ieeexplore.ieee.org\/document\/5457090\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":17,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/date.2010.5457090","relation":{},"subject":[],"published":{"date-parts":[[2010,3]]}}}