{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:13:11Z","timestamp":1729642391009,"version":"3.28.0"},"reference-count":32,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/wsc.2003.1261508","type":"proceedings-article","created":{"date-parts":[[2004,5,6]],"date-time":"2004-05-06T16:18:03Z","timestamp":1083860283000},"page":"888-896","source":"Crossref","is-referenced-by-count":1,"title":["From simulation to verification (and back)"],"prefix":"10.1109","author":[{"given":"H.","family":"Rueb","sequence":"first","affiliation":[]},{"given":"L.","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref32","article-title":"Bounded model checking for timed automata","volume":"68","author":"sorea","year":"2002","journal-title":"ENTCS"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-44518-8_16","article-title":"Symbolic analysis of transition systems","volume":"1912","author":"shankar","year":"2000","journal-title":"In Abstract State Machines Theory and Applications (ASM 2000)"},{"key":"ref30","first-page":"443","article-title":"Abstract and model check while you prove","author":"saidi","year":"1999","journal-title":"See Halbwachs and Peled"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"ref11","first-page":"436","article-title":"Benefits of bounded model checking in an industrial setting","author":"copty","year":"2001","journal-title":"In Computer-Aided Verification CAY 2001 Volume 2101 of LNCS"},{"key":"ref12","article-title":"Lemmas on demand for satisfiability solvers","author":"de moura","year":"2002","journal-title":"SAT 2002"},{"key":"ref13","first-page":"438","article-title":"Lazy theorem proving for bounded model checking over infinite domains","volume":"2392","author":"de moura","year":"2002","journal-title":"Int'l Conference on Automated Deduction (CADE)"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","article-title":"Bounded model checking and induction: From refutation to verification","volume":"2725","author":"de moura","year":"2003","journal-title":"Computer-Aided Verification CAV '2003"},{"key":"ref15","article-title":"The SAL language","author":"dill","year":"2001","journal-title":"Technical Report SRI-CSL-01-02"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2000.896005"},{"key":"ref17","first-page":"246","article-title":"ICS: Integrated Canonization and Solving","volume":"2102","author":"filliatre","year":"2001","journal-title":"In Computer-Aided Venfication CAV '2001"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561318"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49519-3_22"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561320"},{"article-title":"Symbolic model checking","year":"1993","author":"mcmillan","key":"ref27"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"article-title":"A computational logic","year":"1979","author":"boyer","key":"ref6"},{"key":"ref29","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","article-title":"Construction of abstract state graphs with PVS","volume":"1254","author":"saidi","year":"1997","journal-title":"Computer-Aided Verification CAV '97"},{"key":"ref5","first-page":"187","article-title":"An overview of SAL","author":"bensalem","year":"2000","journal-title":"LFM 2000 Fifth NASA Langley Formal Methods Workshop"},{"article-title":"Parallel program design: A foundation","year":"1988","author":"chandy","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded model checking. using satisfiability solving","volume":"19","author":"biere","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_15"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028729"},{"journal-title":"Proceedings 11th Annual IEEE Symposium on Logic in Computer Science","year":"1996","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298864"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384313"},{"key":"ref23","first-page":"359","article-title":"Planning as satisfiability","author":"kautz","year":"1992","journal-title":"In European Conference on A rtificial lntelligence"},{"article-title":"Symbolic model checking","year":"1993","author":"mcmillan","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"}],"event":{"name":"2003 Winter Simulation Conference","acronym":"WSC-03","location":"New Orleans, LA, USA"},"container-title":["Proceedings of the 2003 International Conference on Machine Learning and Cybernetics (IEEE Cat. No.03EX693)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8912\/28195\/01261508.pdf?arnumber=1261508","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,13]],"date-time":"2018-05-13T20:19:45Z","timestamp":1526242785000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1261508\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/wsc.2003.1261508","relation":{},"subject":[]}}