{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:36:36Z","timestamp":1777890996295,"version":"3.51.4"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030684457","type":"print"},{"value":"9783030684464","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-68446-4_9","type":"book-chapter","created":{"date-parts":[[2021,2,12]],"date-time":"2021-02-12T19:06:39Z","timestamp":1613156799000},"page":"173-191","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Reasoning in the Theory of Heap: Satisfiability and Interpolation"],"prefix":"10.1007","author":[{"given":"Zafer","family":"Esen","sequence":"first","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,2,13]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Backeman, P., R\u00fcmmer, P., Zeljic, A.: Bit-vector interpolation and quantifier elimination by lazy reduction. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October\u20132 November 2018, pp. 1\u201310. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603023","DOI":"10.23919\/FMCAD.2018.8603023"},{"issue":"1\u20132","key":"9_CR2","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1\u20132), 21\u201346 (2007)","journal-title":"JSAT"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","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. 7935, pp. 105\u2013125. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_8"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-18275-4_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 88\u2013102. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_8"},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-011-9237-y","volume":"47","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. J. Autom. Reasoning 47, 341\u2013367 (2011)","journal-title":"J. Autom. Reasoning"},{"issue":"1\u20133","key":"9_CR7","doi-asserted-by":"publisher","first-page":"165","DOI":"10.3233\/sat190067","volume":"6","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisfiability Boolean Model. Comput. 6(1\u20133), 165\u2013201 (2009). https:\/\/doi.org\/10.3233\/sat190067","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation of a theory of arrays. Log. Methods Comput. Sci. 8(2) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(2:4)2012","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"9_CR9","unstructured":"Christ, J., Hoenicke, J.: Weakly equivalent arrays. In: R\u00fcmmer, P., Wintersteiger, C.M. (eds.) Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, affiliated with the 26th International Conference on Computer Aided Verification (CAV 2014), the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), and the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria, 17\u201318 July 2014. CEUR Workshop Proceedings, vol. 1163, pp. 39\u201349. CEUR-WS.org (2014). http:\/\/ceur-ws.org\/Vol-1163\/paper-06.pdf"},{"issue":"3","key":"9_CR10","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symbolic Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symbolic Log."},{"issue":"1","key":"9_CR11","doi-asserted-by":"publisher","first-page":"73","DOI":"10.3233\/FI-2017-1461","volume":"150","author":"E De Angelis","year":"2017","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program verification using constraint handling rules and array constraint generalizations. Fundam. Inform. 150(1), 73\u2013117 (2017). https:\/\/doi.org\/10.3233\/FI-2017-1461","journal-title":"Fundam. Inform."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Esen, Z., R\u00fcmmer, P.: Towards an SMT-LIB theory of heap. In: Fribourg, L., Heizmann, M. (eds.) Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT\/HCVS@ETAPS 2020 2020, and 7th Workshop on Horn Clauses for Verification and SynthesisDublin, Ireland, 25\u201326th April 2020. EPTCS, vol. 320 (2020)","DOI":"10.4204\/EPTCS.320.0"},{"key":"9_CR13","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"MC Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving. TCS, 2nd edn. Springer, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","edition":"2"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/978-3-319-94205-6_36","volume-title":"Automated Reasoning","author":"J Hoenicke","year":"2018","unstructured":"Hoenicke, J., Schindler, T.: Efficient interpolation for the theory of arrays. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 549\u2013565. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_36"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: Deciding and interpolating algebraic data types by reduction. In: Jebelean, T., Negru, V., Petcu, D., Zaharie, D., Ida, T., Watt, S.M. (eds.) 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, 21\u201324 September 2017, pp. 145\u2013152. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/SYNASC.2017.00033","DOI":"10.1109\/SYNASC.2017.00033"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October\u20132 November 2018, pp. 1\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"9_CR17","unstructured":"Kahsai, T., Kersten, R., R\u00fcmmer, P., Sch\u00e4f, M.: Quantified heap invariants for object-oriented programs. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7\u201312 May 2017. EPiC Series in Computing, vol. 46, pp. 368\u2013384. EasyChair (2017) https:\/\/easychair.org\/publications\/paper\/Pmh"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT 2006\/FSE-14, pp. 105\u2013116. ACM, New York (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 89\u201396. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846\u2013862. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_59"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_2"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-662-53413-7_18","volume-title":"Static Analysis","author":"D Monniaux","year":"2016","unstructured":"Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361\u2013382. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_18"},{"key":"9_CR23","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, Austin, Texas, USA, 15\u201318 November 2009, pp. 45\u201352. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"3","key":"9_CR25","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-016-9372-6","volume":"58","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reasoning 58(3), 341\u2013362 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9372-6","journal-title":"J. Autom. Reasoning"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7\u201313 June 2008, pp. 159\u2013169. ACM (2008). https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P.: Competition report: CHC-COMP-20. In: Fribourg, L., Heizmann, M. (eds.) Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT\/HCVS@ETAPS 2020 2020, and 7th Workshop on Horn Clauses for Verification and SynthesisDublin, Ireland, 25\u201326th April 2020. EPTCS, vol. 320, pp. 197\u2013219 (2020). https:\/\/doi.org\/10.4204\/EPTCS.320.15","DOI":"10.4204\/EPTCS.320.15"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_24"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, 16\u201319 June 2001, Proceedings, pp. 29\u201337. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932480","DOI":"10.1109\/LICS.2001.932480"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: SIGPLAN Not., vol. 45, no. 1, pp. 199\u2013210 (2010)","DOI":"10.1145\/1707801.1706325"},{"issue":"1","key":"9_CR32","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10817-016-9371-7","volume":"57","author":"N Totla","year":"2016","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. J. Autom. Reasoning 57(1), 37\u201365 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9371-7","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-68446-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T15:53:57Z","timestamp":1619279637000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-68446-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030684457","9783030684464"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-68446-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bologna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nms.kcl.ac.uk\/maribel.fernandez\/LOPSTR2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"In addition, two invited talks are included in the proceedings. Due to the COVID-19 pandemic the conference was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}