{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T21:49:28Z","timestamp":1725745768205},"reference-count":16,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1109\/date.2008.4484777","type":"proceedings-article","created":{"date-parts":[[2008,4,15]],"date-time":"2008-04-15T18:15:51Z","timestamp":1208283351000},"page":"831-836","source":"Crossref","is-referenced-by-count":4,"title":["Completeness in SMT-based BMC for Software Programs"],"prefix":"10.1109","author":[{"given":"Malay K.","family":"Ganai","sequence":"first","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"15","article-title":"checking safety properties using induction and a sat solver","author":"sheeran","year":"2000","journal-title":"Proc of FMCAD"},{"journal-title":"An SMT solver","year":"0","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"14","article-title":"dpll(t) with exhaustive theory propogation and its application to difference logic","author":"nieuwenhuis","year":"2005","journal-title":"Proc of CAV"},{"key":"11","article-title":"f-soft: software verification platform","author":"ivancic","year":"2005","journal-title":"Proc of CAV"},{"key":"12","article-title":"efficient computation of recurrence diamter","author":"kroening","year":"2003","journal-title":"Proc of VMCAI"},{"key":"3","article-title":"symbolic model checking without bdds","author":"biere","year":"1999","journal-title":"Proc of TACAS"},{"key":"2","article-title":"bounded model checking of software using smt solvers instead of sat solvers","author":"armando","year":"2006","journal-title":"Proc of SPIN Workshop"},{"journal-title":"Principles Techniques and Tools","year":"1988","key":"1"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-69167-1"},{"key":"7","article-title":"verification of embedded software: problems and perspectives","author":"cousot","year":"2001","journal-title":"LNCS"},{"key":"6","article-title":"a tool for checking ansi-c programs","author":"clarke","year":"2004","journal-title":"Proc of TACAS"},{"key":"5","article-title":"the mathsat 3 system","author":"bozzano","year":"2005","journal-title":"Proc of CADE"},{"key":"4","article-title":"sat-based verification without state space traversal","author":"bjesse","year":"2000","journal-title":"Proc of FMCAD"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233664"},{"key":"8","article-title":"a fast linear-arithmetic solver for dpll(t)","author":"dutertre","year":"2006","journal-title":"Proc of CAV"}],"event":{"name":"2008 Design, Automation and Test in Europe","start":{"date-parts":[[2008,3,10]]},"location":"Munich, Germany","end":{"date-parts":[[2008,3,14]]}},"container-title":["2008 Design, Automation and Test in Europe"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4475437\/4484624\/04484777.pdf?arnumber=4484777","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,16]],"date-time":"2017-03-16T17:38:52Z","timestamp":1489685932000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4484777\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/date.2008.4484777","relation":{},"subject":[],"published":{"date-parts":[[2008,3]]}}}