{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:11:41Z","timestamp":1773655901417,"version":"3.50.1"},"reference-count":80,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[2015,10,1]],"date-time":"2015-10-01T00:00:00Z","timestamp":1443657600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"European Union\u2019s Seventh Framework Programme","doi-asserted-by":"publisher","award":["FP7\/2007-2013"],"award-info":[{"award-number":["FP7\/2007-2013"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"ERC","doi-asserted-by":"publisher","award":["290914"],"award-info":[{"award-number":["290914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"EU FP7","award":["295261"],"award-info":[{"award-number":["295261"]}]},{"DOI":"10.13039\/501100004343","name":"Swiss SNF","doi-asserted-by":"publisher","award":["200021-134976"],"award-info":[{"award-number":["200021-134976"]}],"id":[{"id":"10.13039\/501100004343","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2015,10,1]]},"DOI":"10.1109\/tse.2015.2431688","type":"journal-article","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T18:32:31Z","timestamp":1431369151000},"page":"1019-1037","source":"Crossref","is-referenced-by-count":26,"title":["Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking"],"prefix":"10.1109","volume":"41","author":[{"given":"Juan P.","family":"Galeotti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eva","family":"May","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gordon","family":"Fraser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Zeller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","first-page":"281","article-title":"DySy: Dynamic symbolic execution for invariant inference","author":"csallner","year":"0","journal-title":"Proc Int Conf Softw Eng"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146255"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568275"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491413"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_15"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00256-7"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"ref75","first-page":"229","article-title":"Automatic generation of program specifications","author":"nimmer","year":"0","journal-title":"Proc Int'l Symp on Softw Testing and Analysis"},{"key":"ref78","first-page":"152","article-title":"Generating test suites with augmented dynamic symbolic execution","author":"jamrozik","year":"0","journal-title":"Proc Tests Proofs"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100092"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"ref31","year":"2008"},{"key":"ref30","year":"2006"},{"key":"ref37","first-page":"72","article-title":"Construction of abstract state graphs with PVS","author":"graf","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"ref35","first-page":"661","article-title":"Apron: A library of numerical abstract domains for static analysis","author":"jeannet","year":"0","journal-title":"Proc 21st Int Conf Comput Aided Verification"},{"key":"ref34","year":"2009"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706326"},{"key":"ref61","article-title":"Inferring invariants in separation logic for imperative list-processing programs","author":"magill","year":"0","journal-title":"Proc 3rd Workshop Semantics Program Anal Comput Environments Memory Manage"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_21"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2529990"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"ref66","first-page":"574","article-title":"A data driven approach for algebraic loop invariants","author":"sharma","year":"0","journal-title":"Proc 22nd Eur Conf Programm Languages Syst"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/781151.781153"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","article-title":"Preliminary design of JML: A behavioral interface specification language for Java","volume":"31","author":"leavens","year":"2006","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2506375"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"},{"key":"ref22","first-page":"634","article-title":"InvGen: An efficient invariant generator","author":"gupta","year":"0","journal-title":"Proc 21st Int Conf Comput Aided Verification"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_15"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_7"},{"key":"ref23","first-page":"164","article-title":"Verification of Java programs using symbolic execution and invariant generation","author":"pasareanu","year":"0","journal-title":"Proc 11th SPIN Workshop"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref25","first-page":"223","article-title":"Program verification using templates over predicate abstraction","author":"gulwani","year":"0","journal-title":"Proc ACM SIGPLAN Conf Programming Language Design and Implementation"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_15"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_14"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_37"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429132"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2009.66"},{"key":"ref54","first-page":"70","article-title":"SAT-based model checking without unrolling","author":"bradley","year":"0","journal-title":"Proc Int Conf Verification Model Checking Abstract Interpretation"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/QSIC.2011.19"},{"key":"ref40","first-page":"195","article-title":"Inferring invariants by symbolic execution","volume":"259","author":"schmitt","year":"0","journal-title":"Proc 4th International Verification Workshop"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1181195.1181200"},{"key":"ref13","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","article-title":"An overview of JML tools and applications","volume":"7","author":"burdy","year":"2005","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref14","first-page":"500","article-title":"Houdini, an annotation assistant for ESC\/Java","author":"flanagan","year":"0","journal-title":"Proc Int 7 Symp Formal Methods Europe on Formal Methods for Increasing Software Productivity"},{"key":"ref15","first-page":"1998","author":"leavens","year":"0"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"ref17","author":"cok","year":"2008"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_8"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1145\/2001576.2001832"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18070-5_2"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_9"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker blast","volume":"9","author":"beyer","year":"2007","journal-title":"Int J Softw Tools for Technol"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926399"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-642-15025-8_15","article-title":"Inferring loop invariants using postconditions","volume":"6300","author":"furia","year":"2010","journal-title":"Fields of Logic and Computation"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"ref7","first-page":"342","article-title":"Beyond assertions: Advanced specification and verification with JML and ESC\/Java2","author":"chalin","year":"0","journal-title":"Proc 4th Int Conf Formal Methods Components Objects"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606572"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_13"},{"key":"ref48","article-title":"Automatically generating loop invariants using quantifier elimination","volume":"5431","author":"kapur","year":"2006","journal-title":"Deduction and Applications"},{"key":"ref47","first-page":"318","article-title":"Non-linear loop invariant generation using Gröbner bases","author":"sankaranarayanan","year":"0","journal-title":"Proceedings of the ACM SIGACT-SIGPLAN Symp Principles of Programming Languages"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214874"},{"key":"ref41","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1016\/j.scico.2010.06.008","article-title":"Predicate abstraction in a program logic calculus","volume":"76","author":"wei\u00df","year":"2011","journal-title":"Sci Comput Program"},{"key":"ref44","first-page":"420","article-title":"Linear invariant generation using non-linear constraint solving","author":"col\u00f3n","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/7297896\/07105412.pdf?arnumber=7105412","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T15:58:06Z","timestamp":1642003086000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7105412\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,1]]},"references-count":80,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tse.2015.2431688","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,10,1]]}}}