{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:18:25Z","timestamp":1749010705372,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415390"},{"type":"electronic","value":"9783319415406"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_12","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"210-229","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Effectively Propositional Interpolants"],"prefix":"10.1007","author":[{"given":"Samuel","family":"Drews","sequence":"first","affiliation":[]},{"given":"Aws","family":"Albarghouthi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-662-46669-8_26","volume-title":"Programming Languages and Systems","author":"A Albargouthi","year":"2015","unstructured":"Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634\u2013660. Springer, Heidelberg (2015)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-39799-8_22","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 313\u2013329. Springer, Heidelberg (2013)"},{"key":"12_CR3","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. 7358, pp. 679\u2013685. Springer, Heidelberg (2012)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Singhania, N.: Precise piecewise affine models from input-output data. In: Mitra, T., Reineke, J. (eds.) EMSOFT, pp. 3:1\u20133:10. ACM (2014)","DOI":"10.1145\/2656045.2656064"},{"issue":"6","key":"12_CR5","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1145\/2666356.2594317","volume":"49","author":"Thomas Ball","year":"2014","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) PLDI, p. 31. ACM (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR6","unstructured":"Bj\u00f8rner, N.: Personal communication"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., Korovin, K., Lahav, O.: Instantiations, zippers and EPR interpolation. In: McMillan, K.L., Middeldorp, A., Sutcliffe, G., Voronkov, A. (eds.) LPAR (short papers). EPiC Series, vol. 26, pp. 35\u201341. EasyChair (2013)","DOI":"10.29007\/xt3j"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"12_CR9","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Model Theory","author":"CC Chang","year":"1973","unstructured":"Chang, C.C., Keisler, J.: Model Theory. Studies in Logic and the Foundations of Mathematics, vol. 73. North-Holland, Amsterdam (1973). 3rd edn., 1990"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-32759-9_17","volume-title":"FM 2012: Formal Methods","author":"E Ermis","year":"2012","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187\u2013201. Springer, Heidelberg (2012)"},{"key":"12_CR11","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 universally quantified invariants of linear data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 813\u2013829. Springer, Heidelberg (2013)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A., Sagiv, M.: Modular reasoning about heap paths via effectively propositional formulas. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 385\u2013396. ACM (2014)","DOI":"10.1145\/2578855.2535854"},{"key":"12_CR14","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. 8044, pp. 756\u2013772. Springer, Heidelberg (2013)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/978-3-319-08867-9_3","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2014","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35\u201351. Springer, Heidelberg (2014)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-21690-4_40","volume-title":"Computer Aided Verification","author":"A Karbyshev","year":"2015","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 583\u2013602. Springer, Heidelberg (2015)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"12_CR20","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 de Moura","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"1","key":"12_CR21","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/2914770.2837640","volume":"51","author":"Oded Padon","year":"2016","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Bodik, R., Majumdar, R. (eds.) POPL, pp. 217\u2013231. ACM (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR22","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: interactive verification of parameterized systems via effectively propositional reasoning. In: PLDI. ACM (2016)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-73595-3_24","volume-title":"Automated Deduction\u2013CADE-21","author":"JA Navarro-P\u00e9rez","year":"2007","unstructured":"Navarro-P\u00e9rez, J.A., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 346\u2013361. Springer, Heidelberg (2007)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-72788-0_2","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2007","author":"JA Navarro-P\u00e9rez","year":"2007","unstructured":"Navarro-P\u00e9rez, J.A., Voronkov, A.: Encodings of problems in effectively propositional logic. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 3\u20133. Springer, Heidelberg (2007)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-642-37651-1_13","volume-title":"Programming Logics","author":"JA Navarro-P\u00e9rez","year":"2013","unstructured":"Navarro-P\u00e9rez, J.A., Voronkov, A.: Planning with effectively propositional logic. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 302\u2013316. Springer, Heidelberg (2013)"},{"issue":"4","key":"12_CR26","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. JAR 44(4), 401\u2013424 (2010)","journal-title":"JAR"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic Implementation of the Best Transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"12_CR28","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. 7358, pp. 71\u201387. Springer, Heidelberg (2012)"},{"issue":"6","key":"12_CR29","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1145\/2813885.2737981","volume":"50","author":"KC Sivaramakrishnan","year":"2015","unstructured":"Sivaramakrishnan, K.C., Kaki, G., Jagannathan, S.: Declarative programming over eventually consistent data stores. In: Grove, D., Blackburn, S. (eds.) PLDI, pp. 413\u2013424. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR30","unstructured":"Thakur, A.: Symbolic Abstraction: Algorithms and Applications. Ph.D. thesis, University of Wisconsin-Madison (2014)"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 537\u2013548. ACM (2013)","DOI":"10.1145\/2480359.2429132"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41540-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:29Z","timestamp":1748997689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}