{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:35:29Z","timestamp":1729629329240,"version":"3.28.0"},"reference-count":20,"publisher":"IEEE Computer Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/icvd.2005.114","type":"proceedings-article","created":{"date-parts":[[2005,3,21]],"date-time":"2005-03-21T20:07:39Z","timestamp":1111435659000},"page":"183-188","source":"Crossref","is-referenced-by-count":1,"title":["Lazy constraints and SAT heuristics for proof-based abstraction"],"prefix":"10.1109","author":[{"family":"Aarti Gupta","sequence":"first","affiliation":[]},{"family":"Malay Ganai","sequence":"additional","affiliation":[]},{"family":"Pranav Ashar","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"17","first-page":"154","article-title":"Counterexample-guided abstraction refinement","volume":"1855","author":"clarke","year":"2000","journal-title":"LNCS"},{"key":"18","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45657-0_20","article-title":"SAT based abstraction-refinement using ILP and machine learning techniques","author":"clarke","year":"2002","journal-title":"Proc Conf Computer-Aided Verification"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2002.1012722"},{"journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach","year":"1994","author":"kurshan","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"14","article-title":"Abstraction and BDDs complement SAT-based BMC in DiVer","volume":"2725","author":"gupta","year":"2003","journal-title":"LNCS"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"12","article-title":"Interpolation and SAT-based model checking","volume":"2725","author":"mcmillan","year":"2003","journal-title":"LNCS"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-9228-4"},{"key":"2","first-page":"272","article-title":"SATO: An efficient propositional prover","volume":"1249","author":"zhang","year":"1997","journal-title":"LNAI"},{"key":"1","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: A search algorithm for prepositional satisfiability","volume":"48","author":"marques-silva","year":"1999","journal-title":"IEEE Transactions on Computers"},{"key":"10","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36577-X_2","article-title":"Automatic abstraction without counterexamples","author":"mcmillan","year":"2003","journal-title":"Proc Tools and Algorithms for the Construction and Analysis of Systems (TACAS 97)"},{"key":"7","doi-asserted-by":"crossref","DOI":"10.1109\/DATE.2003.1253717","article-title":"Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications","author":"zhang","year":"2003","journal-title":"Proceedings of the Design Automation and Test in Europe (DATE)"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"6"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"4","article-title":"Symbolic model checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"LNCS"},{"journal-title":"Proceedings of Conference on Formal Methods in CAD (FMCAD)","article-title":"Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis","year":"2002","author":"chauhan","key":"9"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253718"}],"event":{"name":"18th International Conference on VLSI Design","acronym":"ICVD-05","location":"Kolkata, India"},"container-title":["18th International Conference on VLSI Design held jointly with 4th International Conference on Embedded Systems Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9501\/30140\/01383274.pdf?arnumber=1383274","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,4]],"date-time":"2019-02-04T22:02:01Z","timestamp":1549317721000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1383274\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/icvd.2005.114","relation":{},"subject":[]}}