{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:34Z","timestamp":1763468194262},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319088662"},{"type":"electronic","value":"9783319088679"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_6","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:37:30Z","timestamp":1403955450000},"page":"88-105","source":"Crossref","is-referenced-by-count":56,"title":["From Invariant Checking to Invariant Inference Using Randomized Search"],"prefix":"10.1007","author":[{"given":"Rahul","family":"Sharma","sequence":"first","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-642-31424-7_49","volume-title":"Computer Aided Verification","author":"F. Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 679\u2013685. Springer, Heidelberg (2012)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Amato, G., Parton, M., Scozzari, F.: Discovering invariants via simple component analysis. J. Symb. Comput.\u00a047(12) (2012)","DOI":"10.1016\/j.jsc.2011.12.052"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Andrieu, C., de Freitas, N., Doucet, A., Jordan, M.I.: An Introduction to MCMC for Machine Learning. Machine Learning\u00a050(1) (2003)","DOI":"10.1023\/A:1020281327116"},{"key":"6_CR5","unstructured":"Beyer, D.: Competition on Software Verification (SV-COMP) benchmarks, \n                    \n                      https:\/\/svn.sosy-lab.org\/software\/svbenchmarks\/tags\/svcomp13\/loops\/"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT 9(5-6) (2007)","DOI":"10.1007\/s10009-007-0044-z"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 105\u2013125. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Burnim, J., Jalbert, N., Stergiou, C., Sen, K.: Looper: Lightweight detection of infinite loops at runtime. In: ASE (2009)","DOI":"10.1109\/ASE.2009.87"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Chib, S., Greenberg, E.: Understanding the Metropolis-Hastings Algorithm. The American Statistician 49(4) (1995)","DOI":"10.2307\/2684568"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-642-24559-6_34","volume-title":"Formal Methods and Software Engineering","author":"G. Costantini","year":"2011","unstructured":"Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 505\u2013521. Springer, Heidelberg (2011)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. Weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509511"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3) (2007)","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1007\/978-3-642-39799-8_57","volume-title":"Computer Aided Verification","author":"P. Garg","year":"2013","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: Learning\u00a0universally\u00a0quantified\u00a0invariants of linear\u00a0data\u00a0structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 813\u2013829. Springer, Heidelberg (2013)"},{"key":"6_CR20","series-title":"LNCS","first-page":"69","volume-title":"CAV 2014","author":"P. Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: A Robust Framework for Learning Invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 69\u201386. Springer, Heidelberg (2014)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: FSE (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: POPL (2007)","DOI":"10.1145\/1190216.1190258"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Necula, G.C.: Discovering affine equalities using random interpretation. In: POPL (2003)","DOI":"10.1145\/604131.604138"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-93900-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 120\u2013135. Springer, Heidelberg (2009)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL (2008)","DOI":"10.1145\/1328438.1328459"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 262\u2013276. Springer, Heidelberg (2009)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Harder, M., Mellen, J., Ernst, M.D.: Improving test suites via operational abstraction. In: ICSE (2003)","DOI":"10.1109\/ICSE.2003.1201188"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K. Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1007\/978-3-642-39799-8_53","volume-title":"Computer Aided Verification","author":"S. Itzhaky","year":"2013","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 756\u2013772. Springer, Heidelberg (2013)"},{"key":"6_CR32","unstructured":"Ivancic, F., Sankaranarayanan, S.: NECLA Static Analysis Benchmarks, \n                    \n                      http:\/\/www.nec-labs.com\/research\/system\/systems_SAV-website\/small_static_bench-v1.1.tar.gz"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-11319-2_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Jung","year":"2010","unstructured":"Jung, Y., Kong, S., Wang, B.-Y., Yi, K.: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 180\u2013196. Springer, Heidelberg (2010)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Kannan, Y., Sen, K.: Universal symbolic execution and its application to likely data structure invariant generation. In: ISSTA (2008)","DOI":"10.1145\/1390630.1390665"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-17164-2_23","volume-title":"Programming Languages and Systems","author":"S. Kong","year":"2010","unstructured":"Kong, S., Jung, Y., David, C., Wang, B.-Y., Yi, K.: Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 328\u2013343. Springer, Heidelberg (2010)"},{"key":"6_CR37","unstructured":"McMillan, K., Rybalchenko, A.: Combinatorial approach to some sparse-matrix problems. Tech. rep., Microsoft Research (2013)"},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Naik, M., Yang, H., Castelnuovo, G., Sagiv, M.: Abstractions from tests. In: POPL (2012)","DOI":"10.1145\/2103656.2103701"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Neuwald, A.F., Liu, J.S., Lipman, D.J., Lawrence, C.E.: Extracting protein alignment models from the sequence database. Nucleic Acids Research\u00a025 (1997)","DOI":"10.1093\/nar\/25.9.1665"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE (2012)","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"6_CR42","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Sharma, R.: Termination proofs from tests. In: ESEC\/SIGSOFT FSE (2013)","DOI":"10.1145\/2491411.2491413"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: ASPLOS (2013)","DOI":"10.1145\/2451116.2451150"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 574\u2013592. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Program verification as learning geometric concepts. In: SAS (2013)","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"6_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-31424-7_11","volume-title":"Computer Aided Verification","author":"R. Sharma","year":"2012","unstructured":"Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 71\u201387. Springer, Heidelberg (2012)"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"Sharma, R., Nori, A.V., Aiken, A.: Bias-variance tradeoffs in program analysis. In: POPL (2014)","DOI":"10.1145\/2535838.2535853"},{"key":"6_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-10672-9_3","volume-title":"Programming Languages and Systems","author":"A. Solar-Lezama","year":"2009","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 4\u201313. Springer, Heidelberg (2009)"},{"key":"6_CR50","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI (2009)","DOI":"10.1145\/1542476.1542501"},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a Z3-based string solver for web application analysis. In: ESEC\/SIGSOFT FSE (2013)","DOI":"10.1145\/2491411.2491456"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T05:18:40Z","timestamp":1558934320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}