{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T00:34:42Z","timestamp":1773189282586,"version":"3.50.1"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,3,25]],"date-time":"2016-03-25T00:00:00Z","timestamp":1458864000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,3,25]],"date-time":"2016-03-25T00:00:00Z","timestamp":1458864000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1160904"],"award-info":[{"award-number":["CCF-1160904"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006112","name":"Microsoft Research","doi-asserted-by":"publisher","award":["Fellowship"],"award-info":[{"award-number":["Fellowship"]}],"id":[{"id":"10.13039\/100006112","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-12-2-0020"],"award-info":[{"award-number":["FA8750-12-2-0020"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10703-016-0248-5","type":"journal-article","created":{"date-parts":[[2016,3,25]],"date-time":"2016-03-25T15:57:35Z","timestamp":1458921455000},"page":"235-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["From invariant checking to invariant inference using randomized search"],"prefix":"10.1007","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7527-4653","authenticated-orcid":false,"given":"Rahul","family":"Sharma","sequence":"first","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,25]]},"reference":[{"key":"248_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"12","key":"248_CR2","doi-asserted-by":"publisher","first-page":"1533","DOI":"10.1016\/j.jsc.2011.12.052","volume":"47","author":"G Amato","year":"2012","unstructured":"Amato G, Parton M, Scozzari F (2012) Discovering invariants via simple component analysis. J Symb Comput 47(12):1533\u20131560","journal-title":"J Symb Comput"},{"issue":"1","key":"248_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1020281327116","volume":"50","author":"C Andrieu","year":"2003","unstructured":"Andrieu C, de Freitas N, Doucet A, Jordan MI (2003) An introduction to MCMC for machine learning. Mach Learn 50(1):5\u201343","journal-title":"Mach Learn"},{"key":"248_CR4","unstructured":"Beyer D Competition on Software Verification (SV-COMP) benchmarks. https:\/\/svn.sosy-lab.org\/software\/sv-benchmarks\/tags\/svcomp13\/loops\/"},{"issue":"5\u20136","key":"248_CR5","first-page":"505","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker blast. STTT 9(5\u20136):505\u2013525","journal-title":"The software model checker blast. STTT"},{"key":"248_CR6","doi-asserted-by":"crossref","unstructured":"Beyer D, Henzinger TA, Majumdar R, Rybalchenko A (2007) Invariant synthesis for combined theories. In: VMCAI","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"248_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified horn clauses. In: SAS","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"248_CR8","doi-asserted-by":"crossref","unstructured":"Burckhardt S, Kothari P, Musuvathi M, Nagarakatte S (2010) A randomized scheduler with probabilistic guarantees of finding bugs. In: ASPLOS","DOI":"10.1145\/1736020.1736040"},{"key":"248_CR9","doi-asserted-by":"crossref","unstructured":"Burnim J, Jalbert N, Stergiou C, Sen K (2009) Looper: Lightweight detection of infinite loops at runtime. In: ASE","DOI":"10.1109\/ASE.2009.87"},{"key":"248_CR10","doi-asserted-by":"crossref","unstructured":"Calcagno C, Distefano D, O\u2019Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: POPL","DOI":"10.1145\/1480881.1480917"},{"issue":"4","key":"248_CR11","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1080\/00031305.1995.10476177","volume":"49","author":"S Chib","year":"1995","unstructured":"Chib S, Greenberg E (1995) Understanding the Metropolis-Hastings algorithm. Am Stat 49(4):327\u2013335","journal-title":"Am Stat"},{"key":"248_CR12","doi-asserted-by":"crossref","unstructured":"Claris\u00f3 R, Cortadella J (2004) The octahedron abstract domain. In: SAS","DOI":"10.1007\/978-3-540-27864-1_23"},{"key":"248_CR13","doi-asserted-by":"crossref","unstructured":"Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: TACAS","DOI":"10.1007\/3-540-36577-X_24"},{"key":"248_CR14","doi-asserted-by":"crossref","unstructured":"Col\u00f3n M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: CAV","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"248_CR15","doi-asserted-by":"crossref","unstructured":"Costantini G, Ferrara P, Cortesi A (2011) Static analysis of string values. In: ICFEM","DOI":"10.1007\/978-3-642-24559-6_34"},{"key":"248_CR16","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL","DOI":"10.1145\/512950.512973"},{"key":"248_CR17","doi-asserted-by":"crossref","unstructured":"Dillig I, Dillig T, Aiken A (2010) Fluid updates: beyond strong vs. weak updates. In: ESOP","DOI":"10.1007\/978-3-642-11957-6_14"},{"key":"248_CR18","doi-asserted-by":"crossref","unstructured":"Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA","DOI":"10.1145\/2509136.2509511"},{"issue":"1\u20133","key":"248_CR19","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Prog 69(1\u20133):35\u201345","journal-title":"Sci Comput Prog"},{"key":"248_CR20","doi-asserted-by":"crossref","unstructured":"Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC\/Java. In: FME","DOI":"10.1007\/3-540-45251-6_29"},{"key":"248_CR21","doi-asserted-by":"crossref","unstructured":"Garg P, L\u00f6ding C, Madhusudan P, Neider D (2013) Learning universally quantified invariants of linear data structures. In: CAV","DOI":"10.1007\/978-3-642-39799-8_57"},{"key":"248_CR22","unstructured":"Garg P, L\u00f6ding C, Madhusudan P, Neider D (2014) ICE: a robust learning framework for synthesizing invariants. In: CAV"},{"key":"248_CR23","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI","DOI":"10.1145\/2254064.2254112"},{"key":"248_CR24","doi-asserted-by":"crossref","unstructured":"Gulavani BS, Henzinger TA, Kannan Y, Nori AV, Rajamani SK (2006) Synergy: a new algorithm for property checking. In: FSE","DOI":"10.1145\/1181775.1181790"},{"key":"248_CR25","doi-asserted-by":"crossref","unstructured":"Gulwani S, Jojic N (2007) Program verification as probabilistic inference. In: POPL","DOI":"10.1145\/1190216.1190258"},{"key":"248_CR26","doi-asserted-by":"crossref","unstructured":"Gulwani S, Necula GC (2003) Discovering affine equalities using random interpretation. In: POPL","DOI":"10.1145\/604131.604138"},{"key":"248_CR27","doi-asserted-by":"crossref","unstructured":"Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: PLDI","DOI":"10.1145\/1375581.1375616"},{"key":"248_CR28","doi-asserted-by":"crossref","unstructured":"Gulwani S, Srivastava S, Venkatesan R (2009) Constraint-based invariant inference over predicate abstraction. In: VMCAI","DOI":"10.1007\/978-3-540-93900-9_13"},{"key":"248_CR29","doi-asserted-by":"crossref","unstructured":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu RG (2008) Proving non-termination. In: POPL","DOI":"10.1145\/1328438.1328459"},{"key":"248_CR30","doi-asserted-by":"crossref","unstructured":"Gupta A, Majumdar R, Rybalchenko A (2009) From tests to proofs. In: TACAS","DOI":"10.1007\/978-3-642-00768-2_24"},{"key":"248_CR31","doi-asserted-by":"crossref","unstructured":"Harder M, Mellen J, Ernst MD (2003) Improving test suites via operational abstraction. In: ICSE","DOI":"10.1109\/ICSE.2003.1201188"},{"key":"248_CR32","doi-asserted-by":"crossref","unstructured":"Hoder K, Bj\u00f8rner N (2012) Generalized property directed reachability. In: SAT","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"248_CR33","doi-asserted-by":"crossref","unstructured":"Itzhaky S, Banerjee A, Immerman N, Nanevski A, Sagiv M (2013) Effectively-propositional reasoning about reachability in linked data structures. In: CAV","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"248_CR34","doi-asserted-by":"crossref","unstructured":"Itzhaky S, Bj\u00f8rner N, Reps TW, Sagiv M, Thakur AV (2014) Property-directed shape analysis. In: CAV","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"248_CR35","unstructured":"Ivancic F, Sankaranarayanan S NECLA static analysis benchmarks. http:\/\/www.nec-labs.com\/research\/system\/systems_SAV-website\/small_static_bench-v1.1.tar.gz"},{"key":"248_CR36","doi-asserted-by":"crossref","unstructured":"Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: TACAS. Springer, Berlin","DOI":"10.1007\/11691372_33"},{"key":"248_CR37","doi-asserted-by":"crossref","unstructured":"Jung Y, Kong S, Wang BY, Yi K (2010) Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: VMCAI. Springer, Berlin","DOI":"10.1007\/978-3-642-11319-2_15"},{"key":"248_CR38","doi-asserted-by":"crossref","unstructured":"Kannan Y, Sen K (2008) Universal symbolic execution and its application to likely data structure invariant generation. In: Proceedings of the ISSTA","DOI":"10.1145\/1390630.1390665"},{"key":"248_CR39","doi-asserted-by":"crossref","unstructured":"Kong S, Jung Y, David C, Wang BY, Yi K (2010) Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: APLAS","DOI":"10.1007\/978-3-642-17164-2_23"},{"key":"248_CR40","volume-title":"Combinatorial approach to some sparse-matrix problems","author":"K McMillan","year":"2013","unstructured":"McMillan K, Rybalchenko A (2013) Combinatorial approach to some sparse-matrix problems. Technical report, Microsoft Research"},{"issue":"1","key":"248_CR41","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. High-order Symb Comput 19(1):31\u2013100","journal-title":"High-order Symb Comput"},{"key":"248_CR42","doi-asserted-by":"crossref","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"248_CR43","doi-asserted-by":"crossref","unstructured":"Naik M, Yang H, Castelnuovo G, Sagiv M (2012) Abstractions from tests. In: POPL","DOI":"10.1145\/2103656.2103701"},{"key":"248_CR44","doi-asserted-by":"publisher","first-page":"1665","DOI":"10.1093\/nar\/25.9.1665","volume":"25","author":"AF Neuwald","year":"1997","unstructured":"Neuwald AF, Liu JS, Lipman DJ, Lawrence CE (1997) Extracting protein alignment models from the sequence database. Nucleic Acids Res 25:1665\u20131677","journal-title":"Nucleic Acids Res"},{"key":"248_CR45","doi-asserted-by":"crossref","unstructured":"Nguyen T, Kapur D, Weimer W, Forrest S (2012) Using dynamic analysis to discover polynomial and array invariants. In: ICSE","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"248_CR46","doi-asserted-by":"crossref","unstructured":"Nori AV, Sharma R (2013) Termination proofs from tests. In: ESEC\/SIGSOFT FSE","DOI":"10.1145\/2491411.2491413"},{"key":"248_CR47","doi-asserted-by":"crossref","unstructured":"Qiu X, Garg P, Stefanescu A, Madhusudan P (2013) Natural proofs for structure, data, and separation. In: PLDI","DOI":"10.1145\/2491956.2462169"},{"key":"248_CR48","doi-asserted-by":"crossref","unstructured":"Reps TW, Sagiv S, Yorsh G (2004) Symbolic implementation of the best transformer. In: VMCAI","DOI":"10.1007\/978-3-540-24622-0_21"},{"issue":"3","key":"248_CR49","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv S, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3):217\u2013298","journal-title":"ACM Trans Program Lang Syst"},{"key":"248_CR50","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Chang RM, Jiang G, Ivancic F (2007) State space exploration using feedback constraint generation and monte-carlo sampling. In: ESEC\/SIGSOFT FSE","DOI":"10.1145\/1287624.1287670"},{"key":"248_CR51","doi-asserted-by":"crossref","unstructured":"Schkufza E, Sharma R, Aiken A (2013) Stochastic superoptimization. In: ASPLOS","DOI":"10.1145\/2451116.2451150"},{"key":"248_CR52","doi-asserted-by":"crossref","unstructured":"Sharma R, Aiken A (2014) From invariant checking to invariant inference using randomized search. In: CAV","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"248_CR53","doi-asserted-by":"crossref","unstructured":"Sharma R, Gupta S, Hariharan B, Aiken A, Liang P, Nori AV (2013) A data driven approach for algebraic loop invariants. In: ESOP","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"248_CR54","doi-asserted-by":"crossref","unstructured":"Sharma R, Gupta S, Hariharan B, Aiken A, Nori AV (2013) Program verification as learning geometric concepts. In: SAS","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"248_CR55","doi-asserted-by":"crossref","unstructured":"Sharma R, Nori A, Aiken A (2012) Interpolants as classifiers. In: CAV","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"248_CR56","doi-asserted-by":"crossref","unstructured":"Sharma R, Nori AV, Aiken A (2014) Bias-variance tradeoffs in program analysis. In: POPL","DOI":"10.1145\/2535838.2535853"},{"key":"248_CR57","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A (2009) The sketching approach to program synthesis. In: APLAS","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"248_CR58","doi-asserted-by":"crossref","unstructured":"Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: PLDI","DOI":"10.1145\/1542476.1542501"},{"key":"248_CR59","doi-asserted-by":"crossref","unstructured":"Srivastava S, Gulwani S, Foster JS (2009) VS3: SMT solvers for program verification. In: CAV","DOI":"10.1007\/978-3-642-02658-4_58"},{"key":"248_CR60","doi-asserted-by":"crossref","unstructured":"Zheng Y, Zhang X, Ganesh V (2013) Z3-str: a Z3-based string solver for web application analysis. In: ESEC\/SIGSOFT FSE","DOI":"10.1145\/2491411.2491456"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0248-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0248-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0248-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0248-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,15]],"date-time":"2024-06-15T08:41:53Z","timestamp":1718440913000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0248-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,25]]},"references-count":60,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["248"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0248-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,25]]},"assertion":[{"value":"25 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}