{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T00:35:30Z","timestamp":1773189330078,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_11","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"71-87","source":"Crossref","is-referenced-by-count":84,"title":["Interpolants as Classifiers"],"prefix":"10.1007","author":[{"given":"Rahul","family":"Sharma","sequence":"first","affiliation":[]},{"given":"Aditya V.","family":"Nori","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Refining the control structure of loops using static analysis. In: EMSOFT, pp. 49\u201358 (2009)","DOI":"10.1145\/1629335.1629343"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/3-540-56483-7_20","volume-title":"Machine Learning: From Theory to Applications","author":"A. Blum","year":"1993","unstructured":"Blum, A., Rivest, R.L.: Training a 3-node Neural Network is NP-Complete. In: Hanson, S.J., Rivest, R.L., Remmele, W. (eds.) MIT-Siemens 1993. LNCS, vol.\u00a0661, pp. 9\u201328. Springer, Heidelberg (1993)"},{"key":"11_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1961189.1961199","volume":"2","author":"C.C. Chang","year":"2011","unstructured":"Chang, C.C., Lin, C.J.: LIBSVM: A library for support vector machines. ACM Transactions on Intelligent Systems and Technology\u00a02, 27:1\u201327:27 (2011), software available at http:\/\/www.csie.ntu.edu.tw\/~cjlin\/libsvm","journal-title":"ACM Transactions on Intelligent Systems and Technology"},{"issue":"3","key":"11_CR4","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log.\u00a022(3), 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"issue":"1-3","key":"11_CR5","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":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically Refining Abstract Interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"11_CR7","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":"11_CR8","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI, pp. 375\u2013385 (2009)","DOI":"10.1145\/1543135.1542518"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292 (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning. Springer Series in Statistics. Springer New York Inc. (2001)","DOI":"10.1007\/978-0-387-21606-5"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"11_CR12","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":"11_CR13","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. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00edcek","year":"1997","unstructured":"Kraj\u00edcek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log.\u00a062(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-24310-3_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Becker, B.: Craig Interpolation in the Presence of Non-linear Constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol.\u00a06919, pp. 240\u2013255. Springer, Heidelberg (2011)"},{"key":"11_CR16","unstructured":"Leroux, J., R\u00fcmmer, P.: Craig Interpolation for Presburger Arithmetic in OpenSMT, http:\/\/www.philipp.ruemmer.org\/interpolating-opensmt.shtml"},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci.\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF02187916","volume":"3","author":"N. Megiddo","year":"1988","unstructured":"Megiddo, N.: On the complexity of polyhedral separability. Discrete & Computational Geometry\u00a03, 325\u2013337 (1988)","journal-title":"Discrete & Computational Geometry"},{"key":"11_CR19","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":"11_CR20","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":"11_CR21","doi-asserted-by":"crossref","unstructured":"Platt, J.C.: Fast training of support vector machines using sequential minimal optimization. In: Advances in Kernel Methods: Support Vector Learning, pp. 185\u2013208. MIT Press (1998)","DOI":"10.7551\/mitpress\/1130.003.0016"},{"issue":"3","key":"11_CR22","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log.\u00a062(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"issue":"4","key":"11_CR23","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. J. Symb. Comput.\u00a042(4), 443\u2013476 (2007)","journal-title":"J. Symb. Comput."},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"11_CR25","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":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R. Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying Loop Invariant Generation Using Splitter Predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 703\u2013719. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T20:36:13Z","timestamp":1687552573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}