{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T05:25:19Z","timestamp":1729661119493,"version":"3.28.0"},"reference-count":39,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/memcod.2005.1487912","type":"proceedings-article","created":{"date-parts":[[2005,7,27]],"date-time":"2005-07-27T13:52:28Z","timestamp":1122472348000},"page":"176-185","source":"Crossref","is-referenced-by-count":2,"title":["Three-valued logic in bounded model checking"],"prefix":"10.1109","author":[{"given":"T.","family":"Schuele","sequence":"first","affiliation":[]},{"given":"K.","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","first-page":"1426","article-title":"Bounded model checking and induction: From refutation to verification","volume":"2725","author":"de moura","year":"2003","journal-title":"LNCS"},{"key":"35","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2004.1347504"},{"key":"17","first-page":"85","article-title":"Completeness and complexity of bounded model checking","volume":"2937","author":"clarke","year":"2004","journal-title":"LNCS"},{"key":"36","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","volume":"1954","author":"sheeran","year":"2000","journal-title":"LNCS"},{"key":"18","first-page":"725","article-title":"Tableaux-based model checking in the propositional ?-calculus","volume":"27","author":"cleaveland","year":"1989","journal-title":"Acta Informatica"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_137"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459809"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"16"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4210-9","author":"brzozowski","year":"1995","journal-title":"Asynchronous Circuits"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/990010.990011"},{"journal-title":"Formal analysis of synchronous circuits","year":"1996","author":"shiple","key":"37"},{"key":"11","first-page":"274","article-title":"Model checking partial state spaces with 3-valued temporal logics","volume":"1633","author":"bruns","year":"1999","journal-title":"LNCS"},{"key":"38","first-page":"369","article-title":"Local model checking in the modal ?-calculus","volume":"351","author":"stirling","year":"1989","journal-title":"LNCS"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"21","article-title":"Temporal induction by incremental SAT solving","volume":"89","author":"ee?n","year":"2003","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"20","first-page":"203","article-title":"Using induction and BDDs to model check invariants","volume":"105","author":"de?harbe","year":"1997","journal-title":"IFIP Conference Proceedings"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01053032"},{"key":"23","doi-asserted-by":"crossref","first-page":"55","DOI":"10.3233\/FI-1992-171-205","article-title":"Many-valued modal logics II","volume":"17","author":"fitting","year":"1992","journal-title":"Fundamenta Informat-icae"},{"journal-title":"Introduction to Metamathematics","year":"1952","author":"kleene","key":"24"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580150"},{"key":"26","first-page":"1","article-title":"Interpolation and SAT-based model checking. W. Hunt and F. Somenzi, editors, 7onference on Computer Aided Verification (CAV)","volume":"2725","author":"mcmillan","year":"2003","journal-title":"LNCS"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58940-9"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_2"},{"journal-title":"Verification of Reactive Systems Formal Methods and Algorithms","year":"2003","author":"schneider","key":"29"},{"journal-title":"The Constructive Semantics of Pure Esterel","year":"1999","author":"berry","key":"3"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44977-9_30"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90183-G"},{"key":"1","first-page":"52","article-title":"Cache behavior prediction by abstract interpretation","volume":"1145","author":"alt","year":"1996","journal-title":"LNCS"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1145\/1023833.1023859"},{"key":"7","first-page":"223","article-title":"Iterating transducers in the large","volume":"2725","author":"boigelot","year":"2003","journal-title":"LNCS"},{"key":"6","first-page":"193","article-title":"Symbolic model checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"LNCS"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2005.24"},{"key":"5","doi-asserted-by":"crossref","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advances in Computers"},{"key":"31","article-title":"Improving constructiveness in code generators","author":"schneider","year":"2005","journal-title":"Synchronous Languages Applications and Programming (SLAP)"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-6819-9"},{"key":"8","first-page":"403","article-title":"Regular model checking","volume":"1855","author":"bouajjani","year":"2000","journal-title":"LNCS"}],"event":{"name":"Third ACM & amp; IEEE International Conference on Formal Methods and Models for Co-Design","acronym":"MEMCOD-05","location":"Verona, Italy"},"container-title":["Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9956\/32009\/01487912.pdf?arnumber=1487912","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T23:18:28Z","timestamp":1626218308000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1487912\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/memcod.2005.1487912","relation":{},"subject":[]}}