{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:16:56Z","timestamp":1772043416990,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_31","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T14:35:55Z","timestamp":1361198155000},"page":"574-592","source":"Crossref","is-referenced-by-count":99,"title":["A Data Driven Approach for Algebraic Loop Invariants"],"prefix":"10.1007","author":[{"given":"Rahul","family":"Sharma","sequence":"first","affiliation":[]},{"given":"Saurabh","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Bharath","family":"Hariharan","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]},{"given":"Percy","family":"Liang","sequence":"additional","affiliation":[]},{"given":"Aditya V.","family":"Nori","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the saturn project. In: PASTE, pp. 43\u201348 (2007)","DOI":"10.1145\/1251535.1251543"},{"issue":"12","key":"31_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.: Discovering invariants via simple component analysis. J. Symb. Comput.\u00a047(12), 1533\u20131560 (2012)","journal-title":"J. Symb. Comput."},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11547662_4","volume-title":"Static Analysis","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Rodr\u00edguez-Carbonell, E., Zaffanella, E.: Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 19\u201334. Springer, Heidelberg (2005)"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-33125-1_7","volume-title":"Static Analysis","author":"D. Cachera","year":"2012","unstructured":"Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gr\u00f6bner Bases. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 58\u201374. Springer, Heidelberg (2012)"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-540-27864-1_22","volume-title":"Static Analysis","author":"M.A. Col\u00f3n","year":"2004","unstructured":"Col\u00f3n, M.A.: Approximating the Algebraic Relational Semantics of Imperative Programs. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 296\u2013311. Springer, Heidelberg (2004)"},{"key":"31_CR7","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":"31_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"issue":"1-3","key":"31_CR9","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"M.D. Ernst","year":"2007","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.\u00a069(1-3), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"31_CR10","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: SIGSOFT FSE, pp. 117\u2013127 (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"31_CR11","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":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D. Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving Non-linear Arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"31_CR13","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Inf.\u00a06, 133\u2013151 (1976)","journal-title":"Acta Inf."},{"issue":"7","key":"31_CR14","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-11486-1_21","volume-title":"Perspectives of Systems Informatics","author":"L. Kov\u00e1cs","year":"2010","unstructured":"Kov\u00e1cs, L.: A Complete Invariant Generation Approach for P-solvable Loops. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol.\u00a05947, pp. 242\u2013256. Springer, Heidelberg (2010)"},{"key":"31_CR16","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.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"5","key":"31_CR17","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett.\u00a091(5), 233\u2013244 (2004)","journal-title":"Inf. Process. Lett."},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE, pp. 683\u2013693 (2012)","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications. In: ISSTA, pp. 229\u2013239 (2002)","DOI":"10.1145\/566171.566213"},{"key":"31_CR20","unstructured":"Petter, M.: Berechnung von polynomiellen invarianten. Master\u2019s thesis, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2004)"},{"issue":"1","key":"31_CR21","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","volume":"64","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming\u00a064(1), 54\u201375 (2007)","journal-title":"Science of Computer Programming"},{"issue":"4","key":"31_CR22","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation\u00a042(4), 443\u2013476 (2007)","journal-title":"Journal of Symbolic Computation"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: POPL, pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"key":"31_CR24","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: A data driven approach for algebraic loop invariants. Tech. Report MSR-TR-2012-97, Microsoft Research (2012)"},{"key":"31_CR25","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)"},{"issue":"12","key":"31_CR26","doi-asserted-by":"publisher","first-page":"1945","DOI":"10.1109\/TPAMI.2005.244","volume":"27","author":"R. Vidal","year":"2005","unstructured":"Vidal, R., Ma, Y., Sastry, S.: Generalized principal component analysis (GPCA). IEEE Trans. Pattern Anal. Mach. Intell.\u00a027(12), 1945\u20131959 (2005)","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T04:15:04Z","timestamp":1557548104000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}