{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:00Z","timestamp":1776333540624,"version":"3.51.2"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,5,12]],"date-time":"2021-05-12T00:00:00Z","timestamp":1620777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,5,12]],"date-time":"2021-05-12T00:00:00Z","timestamp":1620777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100011914","name":"M\u00e4lardalen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100011914","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bit-vector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.<\/jats:p>","DOI":"10.1007\/s10703-021-00372-6","type":"journal-article","created":{"date-parts":[[2021,5,12]],"date-time":"2021-05-12T16:03:19Z","timestamp":1620835399000},"page":"121-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic"],"prefix":"10.1007","volume":"57","author":[{"given":"Peter","family":"Backeman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandar","family":"Zelji\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,5,12]]},"reference":[{"key":"372_CR1","doi-asserted-by":"crossref","unstructured":"McMillan KL (2005) An interpolating theorem prover. Theor Comput Sci 345(1):101\u2013121","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"372_CR2","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Purandare M, Weissenbacher G, Kroening D (2010) Interpolant strength. In: VMCAI, LNCS. Springer","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"372_CR3","doi-asserted-by":"crossref","unstructured":"Fuchs A, Goel A, Grundy J, Krsti\u0107 S, Tinelli C (2009) Ground interpolation for the theory of equality. In: TACAS, LNCS. Springer","DOI":"10.1007\/978-3-642-00768-2_34"},{"key":"372_CR4","doi-asserted-by":"crossref","unstructured":"Brillout A, Kroening D, R\u00fcmmer P, Wahl T (2011) Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: VMCAI, LNCS. Springer, pp 88\u2013102","DOI":"10.1007\/978-3-642-18275-4_8"},{"key":"372_CR5","doi-asserted-by":"crossref","unstructured":"McMillan KL (2008) Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems, TACAS 2008, vol 4963 of Lecture Notes in Computer Science. Springer, pp 413\u2013427","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"372_CR6","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs L, Voronkov A (2009) Interpolation and symbol elimination. In: CADE, pp 199\u2013213","DOI":"10.1007\/978-3-642-02959-2_17"},{"issue":"1","key":"372_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-014-9314-0","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina MP, Johansson M (2015) On interpolation in automated theorem proving. J. Autom. Reason. 54(1):69\u201397. https:\/\/doi.org\/10.1007\/s10817-014-9314-0","journal-title":"J. Autom. Reason."},{"key":"372_CR8","doi-asserted-by":"publisher","unstructured":"Kapur D, Majumdar R, Zarba CG (2006) Interpolation for data structures. In: SIGSOFT\u201906\/FSE-14, ACM, New York, NY, USA, pp 105\u2013116. https:\/\/doi.org\/10.1145\/1181775.1181789","DOI":"10.1145\/1181775.1181789"},{"key":"372_CR9","doi-asserted-by":"publisher","unstructured":"Hojjat H, R\u00fcmmer P (2017) Deciding and interpolating algebraic data types by reduction. In: Jebelean T, Negru V, Petcu D, Zaharie D, Ida T, Watt SM (eds) 19th international symposium on symbolic and numeric algorithms for scientific computing, SYNASC 2017, Timisoara, Romania, September 21\u201324, IEEE Computer Society, 2017, pp 145\u2013152. https:\/\/doi.org\/10.1109\/SYNASC.2017.00033","DOI":"10.1109\/SYNASC.2017.00033"},{"key":"372_CR10","doi-asserted-by":"publisher","unstructured":"Dai L, Xia B, Zhan N (2013) Generating non-linear interpolants by semidefinite programming. In: Sharygina N, Veith H (eds) Computer aided verification\u201425th international conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, vol 8044 of Lecture Notes in Computer Science. Springer, pp 364\u2013380. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_25","DOI":"10.1007\/978-3-642-39799-8_25"},{"key":"372_CR11","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 (2011) An interpolating sequent calculus for quantifier-free Presburger arithmetic. J Autom Reason 47:341\u2013367","journal-title":"J Autom Reason"},{"key":"372_CR12","doi-asserted-by":"publisher","unstructured":"Griggio A, Le TTH, Sebastiani R (2010) Efficient interpolant generation in satisfiability modulo linear integer arithmetic. Log Methods Comput Sci. https:\/\/doi.org\/10.2168\/LMCS-8(3:3)2012","DOI":"10.2168\/LMCS-8(3:3)2012"},{"key":"372_CR13","doi-asserted-by":"publisher","unstructured":"Bruttomesso R, Ghilardi S, Ranise S (2012) Quantifier-free interpolation of a theory of arrays. Log Methods Comput Sci. https:\/\/doi.org\/10.2168\/LMCS-8(2:4)2012","DOI":"10.2168\/LMCS-8(2:4)2012"},{"issue":"1","key":"372_CR14","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 (2016) Complete instantiation-based interpolation. J. Autom Reason 57(1):37\u201365. https:\/\/doi.org\/10.1007\/s10817-016-9371-7","journal-title":"J. Autom Reason"},{"key":"372_CR15","doi-asserted-by":"crossref","unstructured":"Hoenicke J, Schindler T (2018) Efficient interpolation for the theory of arrays. CoRR abs\/1804.07173. arXiv:1804.07173","DOI":"10.1007\/978-3-319-94205-6_36"},{"key":"372_CR16","unstructured":"Griggio A (2011) Effective word-level interpolation for software verification. In: Bjesse P, Slobodov\u00e1 A (eds) International conference on formal methods in computer-aided design. FMCAD \u201911, Austin, TX, USA, October 30\u2013November 02, 2011, FMCAD Inc., pp 28\u201336"},{"key":"372_CR17","doi-asserted-by":"publisher","unstructured":"Backeman P, R\u00fcmmer P, Zeljic A Bit-vector interpolation and quantifier elimination by lazy reduction. In: Bj\u00f8rner and Gurfinkel, vol 45, pp. 1\u201310. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603023","DOI":"10.23919\/FMCAD.2018.8603023"},{"key":"372_CR18","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-63166-6_9","volume-title":"Computer aided verification","author":"D Cyrluk","year":"1997","unstructured":"Cyrluk D, M\u00f6ller O, Rue\u00df H (1997) An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg O (ed) Computer aided verification. Springer, Berlin, pp 60\u201371"},{"key":"372_CR19","doi-asserted-by":"publisher","unstructured":"Bruttomesso R, Sharygina N (2009) A scalable decision procedure for fixed-width bit-vectors. In: Proceedings of the 2009 international conference on computer-aided design, ICCAD \u201909, ACM, New York, pp 13\u201320. https:\/\/doi.org\/10.1145\/1687399.1687403","DOI":"10.1145\/1687399.1687403"},{"key":"372_CR20","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: TACAS, vol 7795 of LNCS","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"372_CR21","unstructured":"Asadi S, Blicha M, Fedyukovich G, Hyv\u00e4rinen AEJ, Even-Mendoza K, Sharygina N, Chockler H (2018) Function summarization modulo theories. In: Barthe G, Sutcliffe G, Veanes M (eds) LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, 16-21 November 2018, vol\u00a057 of EPiC Series in Computing, EasyChair, pp 56\u201375"},{"key":"372_CR22","doi-asserted-by":"crossref","unstructured":"Kroening D, Weissenbacher G (2007) Lifting propositional interpolants to the word-level. In: FMCAD, IEEE Computer Society, pp 85\u201389","DOI":"10.1109\/FAMCAD.2007.13"},{"key":"372_CR23","doi-asserted-by":"crossref","unstructured":"Kroening D, Weissenbacher G (2009) An interpolating decision procedure for transitive relations with uninterpreted functions. In: Haifa verification conference, vol 6405 of Lecture Notes in Computer Science. Springer, pp 150\u2013168","DOI":"10.1007\/978-3-642-19237-1_15"},{"key":"372_CR24","doi-asserted-by":"publisher","unstructured":"Ho Y, Chauhan P, Roy P, Mishchenko A, Brayton RK (2016) Efficient uninterpreted function abstraction and refinement for word-level model checking. In: Piskac R, Talupur M (eds), 2016 formal methods in computer-aided design, FMCAD 2016, Mountain View, CA, USA, October 3\u20136, IEEE, 2016, pp 65\u201372. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886662","DOI":"10.1109\/FMCAD.2016.7886662"},{"key":"372_CR25","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P (2008) A constraint sequent calculus for first-order logic with linear integer arithmetic. In: LPAR, vol 5330 of LNCS. Springer, pp 274\u2013289","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"372_CR26","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 MC (1996) First-order logic and automated theorem proving, 2nd edn. Springer, New York","edition":"2"},{"key":"372_CR27","doi-asserted-by":"crossref","unstructured":"Halpern JY (1991) Presburger arithmetic with unary predicates is $$\\Pi _1^1$$ complete. J Symbol Log 56:637\u2013642","DOI":"10.2307\/2274706"},{"issue":"6","key":"372_CR28","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"issue":"3","key":"372_CR29","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds A, King T, Kuncak V (2017) Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst Des 51(3):500\u2013532","journal-title":"Formal Methods Syst Des"},{"issue":"3","key":"372_CR30","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Linear reasoning: a new form of the Herbrand\u2013Gentzen theorem. J Symbol Log 22(3):250\u2013268","journal-title":"J Symbol Log"},{"key":"372_CR31","volume-title":"Algebra","author":"SS Lang","year":"1993","unstructured":"Lang SS (1993) Algebra, 3rd edn. Addison-Wesley, Reading","edition":"3"},{"key":"372_CR32","doi-asserted-by":"crossref","unstructured":"Buchberger B (3, 2006) An algorithm for finding the basis elements in the residue class ring modulo a zero dimensional polynomial ideal, Ph.D. thesis","DOI":"10.1016\/j.jsc.2005.09.007"},{"issue":"2","key":"372_CR33","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1137\/S0036142995281504","volume":"34","author":"P Van Hentenryck","year":"1997","unstructured":"Van Hentenryck P, McAllester D, Kapur D (1997) Solving polynomial systems using a branch and prune approach. SIAM J Numer Anal 34(2):797\u2013827","journal-title":"SIAM J Numer Anal"},{"key":"372_CR34","doi-asserted-by":"crossref","unstructured":"Warren J, Hunt A, Krug RB, Moore JS (2003) Linear and nonlinear arithmetic in ACL2. In: Proceedings, correct hardware design and verification methods, 12th IFIP WG 10.5 advanced research working conference, vol 2860 of LNCS. Springer, pp 319\u2013333","DOI":"10.1007\/978-3-540-39724-3_29"},{"issue":"1","key":"372_CR35","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10817-010-9196-8","volume":"48","author":"C Borralleras","year":"2012","unstructured":"Borralleras C, Lucas S, Oliveras A, Rodr\u00edguez-Carbonell E, Rubio A (2012) SAT modulo linear arithmetic for solving polynomial constraints. J. Autom Reason 48(1):107\u2013131","journal-title":"J. Autom Reason"},{"key":"372_CR36","unstructured":"Barrett C, Fontaine P, Tinelli C (2017) The SMT-LIB Standard: Version 2.6, Technical report, Department of Computer Science, The University of Iowa. www.SMT-LIB.org"},{"key":"372_CR37","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS, vol 4963 of LNCS. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"372_CR38","doi-asserted-by":"publisher","unstructured":"Barrett C, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV, vol 6806 of LNCS. Springer, pp 171\u2013177. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"372_CR39","unstructured":"Beyer D, Keremoglu ME (2009) CPAchecker: a tool for configurable software verification. CoRR abs\/0902.0019. arXiv:0902.0019"},{"key":"372_CR40","doi-asserted-by":"publisher","unstructured":"Hojjat H, R\u00fcmmer P The ELDARICA Horn solver. In: Bj\u00f8rner and Gurfinkel, vol 45, pp 1\u20137. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"372_CR41","doi-asserted-by":"publisher","unstructured":"Demyanova Y, R\u00fcmmer P, Zuleger F (2017) Systematic predicate abstraction using variable roles. In: Barrett C, Davies M, Kahsai T (eds) NASA formal methods\u20149th international symposium, NFM 2017, Moffett Field, CA, USA, May 16\u201318, 2017, Proceedings, vol 10227 of Lecture Notes in Computer Science, pp 265\u2013281. https:\/\/doi.org\/10.1007\/978-3-319-57288-8_18","DOI":"10.1007\/978-3-319-57288-8_18"},{"issue":"4","key":"372_CR42","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s00236-015-0236-z","volume":"53","author":"J Leroux","year":"2016","unstructured":"Leroux J, R\u00fcmmer P, Subotic P (2016) Guiding Craig interpolation with domain-specific abstractions. Acta Inf 53(4):387\u2013424. https:\/\/doi.org\/10.1007\/s00236-015-0236-z","journal-title":"Acta Inf"},{"key":"372_CR43","doi-asserted-by":"publisher","unstructured":"Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: Hosking AL, Eugster PT, Lopes CV (eds), Proceedings of the 2013 ACM SIGPLAN international conference on object oriented programming systems languages & applications, OOPSLA. ACM, pp 443\u2013456. https:\/\/doi.org\/10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"372_CR44","doi-asserted-by":"publisher","unstructured":"Beyer D, Cimatti A, Griggio A, Keremoglu ME, Sebastiani R (2009) Software model checking via large-block encoding. In: Proceedings of 9th international conference on formal methods in computer-aided design, FMCAD 2009, 15\u201318 November 2009, Austin, Texas, USA. IEEE, pp 25\u201332. https:\/\/doi.org\/10.1109\/FMCAD.2009.5351147","DOI":"10.1109\/FMCAD.2009.5351147"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00372-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00372-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00372-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T18:12:14Z","timestamp":1636481534000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00372-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,12]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["372"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00372-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,5,12]]},"assertion":[{"value":"25 March 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 May 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}