{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T17:51:54Z","timestamp":1729619514741,"version":"3.28.0"},"reference-count":10,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,11]]},"DOI":"10.1109\/hldvt.2008.4695874","type":"proceedings-article","created":{"date-parts":[[2008,12,10]],"date-time":"2008-12-10T16:43:50Z","timestamp":1228927430000},"page":"49-55","source":"Crossref","is-referenced-by-count":0,"title":["Multi-level Bounded Model Checking to detect bugs beyond the bound"],"prefix":"10.1109","author":[{"family":"Tasuku Nishihara","sequence":"first","affiliation":[]},{"family":"Takeshi Matsumoto","sequence":"additional","affiliation":[]},{"family":"Masahiro Fujita","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"3","first-page":"108","article-title":"checking safety properties using induction and a sat-solver","author":"sheeran","year":"2000","journal-title":"Proc of FMCAD"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"10","first-page":"154","article-title":"counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"Proc of CAV"},{"key":"1","first-page":"118","article-title":"bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advances in Computers"},{"key":"7","first-page":"359","article-title":"nusmv 2: an opensource tool for symbolic model checking","author":"cimatti","year":"2002","journal-title":"Proc of CAV"},{"journal-title":"RTL Semantics draft specification","year":"0","key":"6"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3636-9"},{"key":"4","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11513988_10","article-title":"incremental and complete bounded model checking for full pltl","volume":"3576","author":"heljanko","year":"2005","journal-title":"Lecture Notes in Computer Science"},{"key":"9","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1145\/1005285.1005324","article-title":"automatic generation of polynomial loop invariants: algebraic foundations","author":"rodriguez-carbonell","year":"2004","journal-title":"Proc Int Symp Symbolic Algebraic Comput ISSAC'02"},{"key":"8","first-page":"330","article-title":"computing interprocedurally valid relations in affine programs","author":"olm","year":"2004","journal-title":"Proc of POPL"}],"event":{"name":"2008 IEEE International High Level Design Validation and Test Workshop (HLDVT)","start":{"date-parts":[[2008,11,19]]},"location":"Incline Village, NV, USA","end":{"date-parts":[[2008,11,21]]}},"container-title":["2008 IEEE International High Level Design Validation and Test Workshop"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4690895\/4695856\/04695874.pdf?arnumber=4695874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,22]],"date-time":"2023-05-22T20:58:18Z","timestamp":1684789098000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4695874\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11]]},"references-count":10,"URL":"https:\/\/doi.org\/10.1109\/hldvt.2008.4695874","relation":{},"subject":[],"published":{"date-parts":[[2008,11]]}}}