{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T00:22:40Z","timestamp":1787530960895,"version":"build-2736575974"},"reference-count":37,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/ase.2017.8115691","type":"proceedings-article","created":{"date-parts":[[2017,11,23]],"date-time":"2017-11-23T22:03:57Z","timestamp":1511474637000},"page":"804-814","source":"Crossref","is-referenced-by-count":9,"title":["Symlnfer: Inferring program invariants using symbolic states"],"prefix":"10.1109","author":[{"given":"ThanhVu","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref33","first-page":"634","article-title":"Invgen: An efficient invariant generator","author":"gupta","year":"2009","journal-title":"CAV"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"ref31","first-page":"443","article-title":"Inductive invariant generation via abductive inference","author":"dillig","year":"2013","journal-title":"OOPSLA"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1145\/1480881.1480898","article-title":"SPEED: precise and efficient static estimation of program computational complexity","author":"gulwani","year":"2009","journal-title":"POPL"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"ref36","first-page":"95","article-title":"Directed symbolic execution","author":"ma","year":"2011","journal-title":"SAS"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"ref34","author":"jeannet","year":"2014","journal-title":"Interproc Analyzer for Recursive Programs with Numerical Variables"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"ref11","first-page":"608","article-title":"Using Dynamic Analysis to Generate Disjunctive Invariants","year":"2014","journal-title":"ICSE"},{"key":"ref12","first-page":"30:1","article-title":"DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants","volume":"23","year":"2014","journal-title":"TOSEM"},{"key":"ref13","first-page":"21","article-title":"The Astrée analyzer","author":"cousot","year":"2005","journal-title":"ESOP"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.53"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"ref16","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"OSDI'10 USENIX Association"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45139-0_7"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"ref28","first-page":"574","article-title":"A data-driven approach for algebraic loop invariants","author":"sharma","year":"2013","journal-title":"ESOP"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173734"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629585"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"ref29","first-page":"51","article-title":"SPEED: Symbolic complexity bound analysis","author":"gulwani","year":"2009","journal-title":"CAV"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610389"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"ref2","author":"ernst","year":"2000","journal-title":"Dynamically Detecting Likely Program Invariants"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_12"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"ref20","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"TACAS"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831716"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111042"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/781151.781153"},{"key":"ref26","author":"stein","year":"2017","journal-title":"SAGE Mathematics Software"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"}],"event":{"name":"2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)","location":"Urbana, IL","start":{"date-parts":[[2017,10,30]]},"end":{"date-parts":[[2017,11,3]]}},"container-title":["2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8106906\/8115603\/08115691.pdf?arnumber=8115691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,29]],"date-time":"2023-08-29T01:13:58Z","timestamp":1693271638000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8115691\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":37,"URL":"https:\/\/doi.org\/10.1109\/ase.2017.8115691","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}