{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T16:21:24Z","timestamp":1743265284530},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1109\/date.2008.4484757","type":"proceedings-article","created":{"date-parts":[[2008,4,15]],"date-time":"2008-04-15T22:15:51Z","timestamp":1208297751000},"page":"682-687","source":"Crossref","is-referenced-by-count":7,"title":["Simulation-Directed Invariant Mining for Software Verification"],"prefix":"10.1109","author":[{"given":"Xueqi","family":"Cheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael S.","family":"Hsiao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503275"},{"key":"15","first-page":"227","article-title":"joining dataflow with predicates","author":"fischer","year":"2005","journal-title":"Proceedings of 13th Intl Symposium on Foundations of Software Engineering"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"journal-title":"Flow Analysis of Computer Programs","year":"1977","author":"hecht","key":"13"},{"key":"14","first-page":"113","article-title":"a technique for invariant generation","author":"tiwari","year":"2001","journal-title":"Proc of TACAS"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/69.250074"},{"key":"12","article-title":"an extensible sat-solver","author":"ee?n","year":"2003","journal-title":"Proc of 6th Intl Conf on Theory and Applications of Satisfiability Testing"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233664"},{"key":"2","first-page":"108","article-title":"checking safety properties using induction and a sat solver","author":"sheeran","year":"2000","journal-title":"FMCAD"},{"key":"1","article-title":"symbolic model checking without bdds","author":"biere","year":"1999","journal-title":"LNCS"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/170035.170072"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_15"},{"key":"6","first-page":"168","article-title":"a tool for checking ansi-c programs","author":"clarke","year":"2004","journal-title":"Proc of TACAS"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/1146909.1147098"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"9","article-title":"verification of java programs using symbolic execution and invariant generation","author":"pasareanu","year":"2004","journal-title":"SPI Proc"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989812"}],"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\/04484757.pdf?arnumber=4484757","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,16]],"date-time":"2017-03-16T15:50:24Z","timestamp":1489679424000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4484757\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1109\/date.2008.4484757","relation":{},"subject":[],"published":{"date-parts":[[2008,3]]}}}