{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T09:49:25Z","timestamp":1764841765805},"reference-count":78,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,5,21]],"date-time":"2014-05-21T00:00:00Z","timestamp":1400630400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10703-014-0209-9","type":"journal-article","created":{"date-parts":[[2014,5,20]],"date-time":"2014-05-20T02:01:10Z","timestamp":1400551270000},"page":"63-109","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["An extension of lazy abstraction with interpolation for programs with arrays"],"prefix":"10.1007","volume":"45","author":[{"given":"Francesco","family":"Alberti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,5,21]]},"reference":[{"issue":"2","key":"209_CR1","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla PA, Jonsson B (1996) Verifying programs with unreliable channels. Inf Comput 127(2):91\u2013101","journal-title":"Inf Comput"},{"key":"209_CR2","unstructured":"Aho AV, Lam MS, Sethi R, Ullman JD (2007) Compilers: principles, techniques, and tools, 2nd edn. Pearson-Addison Wesley."},{"key":"209_CR3","first-page":"300","volume-title":"SAS","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) Craig interpretation. In: Min\u00e9 A, Schmidt D (eds) SAS. Springer, Lecture Notes in Computer Science, pp 300\u2013316"},{"key":"209_CR4","doi-asserted-by":"crossref","unstructured":"Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N (2012) Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner N, Voronkov A (eds) LPAR, Lecture Notes in Computer Science, vol 7180, pp 46\u201361. Springer.","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"209_CR5","doi-asserted-by":"crossref","unstructured":"Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N (2012) SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan P, Seshia SA (eds) CAV., Lecture Notes in Computer Science, vol 7358, Springer, Berlin, pp 679\u2013685","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"209_CR6","doi-asserted-by":"crossref","unstructured":"Alberti F, Ghilardi S, Pagani E, Ranise S, Rossi GP (2010). Automated support for the design and validation of fault tolerant parameterized systems: a case study. ECEASST, p 35.","DOI":"10.1007\/978-3-642-15763-9_36"},{"issue":"1\/2","key":"209_CR7","first-page":"29","volume":"8","author":"F Alberti","year":"2012","unstructured":"Alberti F, Ghilardi S, Pagani E, Ranise S, Rossi GP (2012) Universal guards, relativization of quantifiers, and failure models in Model Checking Modulo theories. JSAT 8(1\/2):29\u201361","journal-title":"JSAT"},{"key":"209_CR8","doi-asserted-by":"crossref","unstructured":"Armando A, Benerecetti M, Carotenuto D, Mantovani J, Spica P (2007) The Eureka tool for software model checking. In Stirewalt REK, Egyed A, Fischer B (eds), ASE. ACM, pp 541\u2013542.","DOI":"10.1145\/1321631.1321734"},{"key":"209_CR9","doi-asserted-by":"crossref","unstructured":"Armando A, Benerecetti M, Mantovani J (2007). Abstraction refinement of linear programs with arrays. In: Grumberg O, Huth M (eds) TACAS, Lecture Notes in Computer Science, vol 4424. Springer, pp 373\u2013388.","DOI":"10.1007\/978-3-540-71209-1_29"},{"key":"209_CR10","doi-asserted-by":"crossref","first-page":"535","DOI":"10.2178\/jsl\/1185803623","volume":"72","author":"Baader Franz","year":"2007","unstructured":"Franz Baader, Silvio Ghilardi (2007) Connecting many-sorted theories. J Symb Logic 72:535\u2013583","journal-title":"Connecting many-sorted theories. J Symb Logic"},{"key":"209_CR11","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Launchbury and Mitchell (eds) Conference record of POPL 2002: The 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16\u201318, 2002. ACM, pp 1\u20133.","DOI":"10.1145\/503272.503274"},{"key":"209_CR12","unstructured":"Beyer D (2013) Second competition on Software Verification\u2013(Summary of SV-COMP 2013). In Piterman N, Smolka SA (eds) Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Lecture Notes in Computer Science, vol 7795. Springer, pp 594\u2013609"},{"key":"209_CR13","doi-asserted-by":"crossref","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker blast. STTT 9(5\u20136):505\u2013525","DOI":"10.1007\/s10009-007-0044-z"},{"key":"209_CR14","doi-asserted-by":"crossref","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R, Rybalchenko A (2007) Invariant synthesis for combined theories. In Cook B, Podelski A (eds) VMCAI, Lecture Notes in Computer Science, vol 4349. Springer, pp 378\u2013394.","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"209_CR15","doi-asserted-by":"crossref","unstructured":"Beyer D, Erkan Keremoglu M (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Lecture Notes in Computer Science, vol 6806. Springer pp 184\u2013190.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"209_CR16","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti AA, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland R (ed) TACAS, Lecture Notes in Computer Science, vol 1579. Springer, pp 193\u2013207.","DOI":"10.21236\/ADA360973"},{"key":"209_CR17","doi-asserted-by":"crossref","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T\u00c6, Schmidt DA, Sudborough IH (eds) The essence of computation, Lecture Notes in Computer Science, vol 2566. Springer, pp 85\u2013108.","DOI":"10.1007\/3-540-36377-7_5"},{"key":"209_CR18","doi-asserted-by":"crossref","unstructured":"Brillout A, Kroening, D, R\u00fcmmer P, Wahl T (2010) An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Giesl H (ed) Proceedings of the 5th international joint conference on automated reasoning, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Lecture Notes in Computer Science, vol 6173. Springer, pp 384\u2013399.","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"209_CR19","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Ghilardi S, Ranise S (2012) From strong amalgamability to modularity of quantifier-free interpolation. In: IJCAR, Lecture Notes in Computer Science. Springer, pp 118\u2013133.","DOI":"10.1007\/978-3-642-31365-3_12"},{"key":"209_CR20","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Ghilardi S, Ranise S (2012) Quantifier-free interpolation of a theory of arrays. Logical Methods in Computer Science 8(2)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"209_CR21","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT solver. In: Esparza J, Majumdar R (eds) TACAS, Lecture Notes in Computer Science, vol 6015. Springer, pp 150\u2013153.","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"209_CR22","doi-asserted-by":"crossref","unstructured":"Carioni A, Ghilardi S, Ranise S (2011) Automated termination in model checking Modulo theories. In: Delzanno G, Potapov I (eds) RP, Lecture Notes in Computer Science, vol 6945. Springer, pp 110\u2013124.","DOI":"10.1007\/978-3-642-24288-5_11"},{"key":"209_CR23","doi-asserted-by":"crossref","unstructured":"Chase DR, Wegman MN, Zadeck FK (1990) Analysis of pointers and structures. In: Fischer BN (ed) PLDI. ACM, pp 296\u2013310.","DOI":"10.1145\/93542.93585"},{"key":"209_CR24","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: Piterman N, Smolka SA (eds) Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Lecture Notes in Computer Science, vol 7795. Springer, pp 93\u2013107.","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"1","key":"209_CR25","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.scico.2006.03.009","volume":"64","author":"Claris\u00f3 Robert","year":"2007","unstructured":"Robert Claris\u00f3, Jordi Cortadella (2007) The octahedron abstract domain. Sci Comput Program 64(1):115\u2013139","journal-title":"Sci Comput Program"},{"key":"209_CR26","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Allen Emerson E, Prasad Sistla A (eds) CAV, Lecture Notes in Computer Science, vol 1855. Springer, pp 154\u2013169.","DOI":"10.1007\/10722167_15"},{"key":"209_CR27","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In Jensen K, Podelski A (eds) TACAS, Lecture Notes in Computer Science, vol 2988. Springer, pp 168\u2013176.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"209_CR28","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham RM, Harrison MA, Sethi R (eds) POPL. ACM, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"209_CR29","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R, Logozzo F (2011) A parametric segmentation functor for fully automatic and scalable array content analysis. In Ball T, Sagiv M (eds) POPL. ACM, pp 105\u2013118.","DOI":"10.1145\/1926385.1926399"},{"key":"209_CR30","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Aho Alfred V, Zilles Stephen N, Szymanski Thomas G (eds) POPL. ACM Press, pp 84\u201396.","DOI":"10.1145\/512760.512770"},{"issue":"3","key":"209_CR31","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269\u2013285","journal-title":"J Symb Log"},{"key":"209_CR32","unstructured":"Mendon\u00e7a de Moura L, Bj\u00f8rner N (2007) Efficient e-matching for SMT solvers. In Pfenning F (ed) CADE, Lecture Notes in Computer Science, vol 4603. Springer, pp 183\u2013198."},{"key":"209_CR33","unstructured":"Mendon\u00e7a de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008, Lecture Notes in Computer Science, vol 4963. Springer, pp 337\u2013340."},{"key":"209_CR34","first-page":"50","volume":"1683","author":"G Delzanno","year":"1999","unstructured":"Delzanno G, Esparza J, Podelski A (1999) Constraint-based analysis of broadcast protocols. Proceedings of CSL, LNCS 1683:50\u201366","journal-title":"Proceedings of CSL, LNCS"},{"key":"209_CR35","unstructured":"Dillig I, Dillig T, Alex Aiken T (2010) Fluid updates: beyond strong vs. weak updates. In Gordon AD (ed), ESOP, Lecture Notes in Computer Science, vol 6012. Springer, pp 246\u2013266."},{"key":"209_CR36","unstructured":"Dimitrova R, Podelski A (2008) Is lazy abstraction a decision procedure for broadcast protocols? In: Logozzo F, Peled D, Zuck LD (eds) VMCAI, Lecture Notes in Computer Science, vol. 4905. Springer, pp 98\u2013111."},{"key":"209_CR37","doi-asserted-by":"crossref","unstructured":"Dudka K, Peringer P, Vojnar T (2011) Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Lecture Notes in Computer Science, vol 6806. Springer, pp 372\u2013378.","DOI":"10.1007\/978-3-642-22110-1_29"},{"key":"209_CR38","doi-asserted-by":"crossref","unstructured":"Dudka K, Peringer P, Vojnar T (2013) Byte-precise verification of low-level list manipulation. In: Logozzo F, F\u00e4hndrich M (eds) SAS, Lecture Notes in Computer Science, vol 7935. Springer, pp 215\u2013237.","DOI":"10.1007\/978-3-642-38856-9_13"},{"key":"209_CR39","doi-asserted-by":"crossref","unstructured":"Enderton HB (2001) A Mathematical introduction to logic. Elsevier Science.","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"209_CR40","unstructured":"F\u00e4hndrich M, Logozzo F (2010) Static contract checking with abstract interpretation. In Beckert B, March\u00e9 C (eds) FoVeOOS, Lecture Notes in Computer Science, vol 6528. Springer, pp 10\u201330."},{"key":"209_CR41","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qadeer S (2002) Predicate abstraction for software verification. In: Launchbury J, Mitchell JC (eds) Conference record of POPL 2002: the 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16\u201318, 2002. ACM, pp 191\u2013202.","DOI":"10.1145\/503272.503291"},{"key":"209_CR42","doi-asserted-by":"crossref","unstructured":"Furia C.A., Meyer B. (2010). Inferring loop invariants using postconditions. In A. Blass, N. Dershowitz, and W. Reisig (eds), Fields of Logic and Computation, volume 6300 of Lecture Notes in Computer Science, pages 277\u2013300. Springer.","DOI":"10.1007\/978-3-642-15025-8_15"},{"issue":"1\u20132","key":"209_CR43","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/s10472-009-9153-6","volume":"55","author":"Y Ge","year":"2009","unstructured":"Ge Y, Barrett CW, Tinelli C (2009) Solving quantified verification conditions using Satisfiability Modulo Theories. Ann. Math. Artif. Intell. 55(1\u20132):101\u2013122","journal-title":"Ann. Math. Artif. Intell."},{"key":"209_CR44","doi-asserted-by":"crossref","unstructured":"Ge Y, Mendon\u00e7a de Moura L (2009) Complete instantiation for quantified formulas in Satisfiabiliby Modulo Theories. In Bouajjani A, Maler O (eds) CAV, Lecture Notes in Computer Science, vol 5643. Springer, pp 306\u2013320.","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"209_CR45","unstructured":"Ghilardi S, Ranise S (2009) Model checking Modulo theory at work: the integration of Yices in MCMT. In: AFM."},{"key":"209_CR46","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Ranise S (2010) Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Logical Methods in Computer Science 6(4)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"209_CR47","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Ranise S (2010) Mcmt: a model checker modulo theories. In Giesl J, H\u00e4hnle R (eds) Proceedings of the 5th international joint conference on automated reasoning, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Lecture Notes in Computer Science, vol 6173. Springer, pp 22\u201329.","DOI":"10.1007\/978-3-642-14203-1_3"},{"issue":"2","key":"209_CR48","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.entcs.2009.08.019","volume":"250","author":"S Ghilardi","year":"2009","unstructured":"Ghilardi S, Ranise S, Valsecchi T (2009) Light-weight SMT-based model checking. Electron Notes Theor Comput Sci 250(2):85\u2013102","journal-title":"Electron Notes Theor Comput Sci"},{"key":"209_CR49","doi-asserted-by":"crossref","unstructured":"Gopan D, Reps TW, Sagiv S (2005) A framework for numeric analysis of array operations. In: Palsberg J, Abadi M (eds) POPL. ACM, pp 338\u2013350.","DOI":"10.1145\/1040305.1040333"},{"key":"209_CR50","doi-asserted-by":"crossref","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In Grumberg O (ed) CAV, Lecture Notes in Computer Science, vol 1254. Springer, pp 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"209_CR51","doi-asserted-by":"crossref","unstructured":"Gulwani S, Tiwari A (2006) Combining abstract interpreters. In: Schwartzbach MI, Ball T (eds) PLDI. ACM, pp 376\u2013386.","DOI":"10.1145\/1133981.1134026"},{"key":"209_CR52","doi-asserted-by":"crossref","unstructured":"Halbwachs N, P\u00e9ron M (2008) Discovering properties about arrays in simple programs. In Gupta R, Amarasinghe SP (eds) PLDI. ACM, pp 339\u2013348.","DOI":"10.1145\/1375581.1375623"},{"key":"209_CR53","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: Jones ND, Leroy X (eds) POPL. ACM, pp 232\u2013244.","DOI":"10.1145\/964001.964021"},{"key":"209_CR54","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Launchbury J, Mitchell JC (eds) Conference record of POPL 2002: the 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16\u201318, 2002. ACM, pp 58\u201370.","DOI":"10.1145\/503272.503279"},{"key":"209_CR55","unstructured":"Hind M (2001) Pointer analysis: haven\u2019t we solved this problem yet? In: Field J, Snelting G (eds) PASTE. ACM, pp 54\u201361."},{"key":"209_CR56","doi-asserted-by":"crossref","unstructured":"Hoder K, Kov\u00e1cs L, Voronkov A (2010) Interpolation and symbol elimination in Vampire. In: Giesl H (ed) Proceedings of the 5th international joint conference on automated reasoning, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Lecture Notes in Computer Science, vol 6173. Springer, pp 188\u2013195.","DOI":"10.1007\/978-3-642-14203-1_16"},{"key":"209_CR57","unstructured":"Hodges W (1993) Model theory, volume 42 of encyclopedia of mathematics and its applications. Cambridge University Press, Cambridge."},{"key":"209_CR58","doi-asserted-by":"crossref","unstructured":"Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: Hermanns H, Palsberg J (eds) TACAS, Lecture Notes in Computer Science, vol 3920. Springer, pp 459\u2013473.","DOI":"10.1007\/11691372_33"},{"key":"209_CR59","doi-asserted-by":"crossref","unstructured":"Jhala R, McMillan KL (2007) Array abstractions from proofs. In Damm W, Hermanns H (eds) CAV, Lecture Notes in Computer Science, vol 4590. Springer, pp 193\u2013206.","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"209_CR60","doi-asserted-by":"crossref","unstructured":"Kapur D, Majumdar R, Zarba CG (2006) Interpolation for data structures. In: Young M, Devanbu PT (eds) SIGSOFT FSE. ACM, pp 105\u2013116.","DOI":"10.1145\/1181775.1181789"},{"key":"209_CR61","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs L, Voronkov A (2009) Finding loop invariants for programs over arrays using a theorem prover. In Chechik M, Wirsing M (eds) FASE, Lecture Notes in Computer Science, vol 5503. Springer, pp 470\u2013485.","DOI":"10.1109\/SYNASC.2009.66"},{"key":"209_CR62","unstructured":"Lahiri SK, Bryant RE (2004) Constructing quantified invariants via predicate abstraction. In Steffen B, Levi G (eds) VMCAI, Lecture Notes in Computer Science, vol 2937. Springer, pp 267\u2013281."},{"key":"209_CR63","unstructured":"Lahiri SK, Bryant RE (2004) Indexed predicate discovery for unbounded system verification. In Alur R, Peled D (eds) CAV, Lecture Notes in Computer Science, vol. 3114. Springer, pp 135\u2013147."},{"key":"209_CR64","doi-asserted-by":"crossref","unstructured":"Larraz D, Rodr\u00edguez-Carbonell E, Rubio A (2013) SMT-based array invariant generation. In: Giacobazzi R, Berdine J, Mastroeni I (eds) VMCAI, Lecture Notes in Computer Science, vol 7737. Springer, pp 169\u2013188.","DOI":"10.1007\/978-3-642-35873-9_12"},{"key":"209_CR65","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems\u2013specification","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems\u2013specification. Springer, Berlin"},{"key":"209_CR66","unstructured":"McCarthy J (1962) Towards a mathematical science of computation. In: IFIP Congress, pp 21\u201328."},{"key":"209_CR67","doi-asserted-by":"crossref","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: Ball T, Jones RB (eds) Proceedings of the 18th international conference on computer aided verification, CAV 2006, Seattle, WA, USA, August 17\u201320, 2006, Lecture Notes in Computer Science, vol 4144. Springer, pp 123\u2013136.","DOI":"10.1007\/11817963_14"},{"key":"209_CR68","doi-asserted-by":"crossref","unstructured":"McMillan KL (2008) Quantified invariant generation using an interpolating saturation prover. In Ramakrishnan CR, Rehof J (eds) Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March\u2013April 6, 2008, Lecture Notes in omputer Science, vol 4963. Springer, pp 413\u2013427.","DOI":"10.1007\/978-3-540-78800-3_31"},{"issue":"1","key":"209_CR69","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"Min\u00e9 Antoine","year":"2006","unstructured":"Antoine Min\u00e9 (2006) The octagon abstract domain. Higher-Order Symb Comput 19(1):31\u2013100","journal-title":"Higher-Order Symb Comput"},{"issue":"2","key":"209_CR70","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson G, Oppen DC (1979) Simplification by Cooperating Decision Procedures. ACM Trans Program Lang Syst 1(2):245\u2013257","journal-title":"ACM Trans Program Lang Syst"},{"key":"209_CR71","doi-asserted-by":"crossref","unstructured":"Podelski A, Wies T (2005) Boolean heaps. In Hankin C, Siveroni I (eds) SAS, Lecture Notes in Computer Science, vol 3672. Springer, pp 268\u2013283.","DOI":"10.1007\/11547662_19"},{"key":"209_CR72","unstructured":"Ranise S, Tinelli C (2006). The satisfiability Modulo theories library (SMT-LIB). http:\/\/www.smt-lib.orgwww.SMT-LIB.org"},{"key":"209_CR73","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: LICS. IEEE Computer Society, pp 55\u201374.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"209_CR74","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Suboti\u0107 P (2013) Exploring interpolants. In: Jobstmann B, Ray S (eds) FMCAD. FMCAD Inc., pp 69\u201376.","DOI":"10.1109\/FMCAD.2013.6679393"},{"key":"209_CR75","unstructured":"Sagiv S, Reps TW, Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. In: Appel AW, Aiken A (eds) POPL. ACM, pp 105\u2013118 (1999)."},{"key":"209_CR76","doi-asserted-by":"crossref","unstructured":"Seghir MN, Podelski A, Wies T (2009) Abstraction refinement for quantified array assertions. In: Palsberg J, Su Z (eds) SAS, Lecture Notes in Computer Science, vol 5673. Springer, pp 3\u201318.","DOI":"10.1007\/978-3-642-03237-0_3"},{"key":"209_CR77","doi-asserted-by":"crossref","unstructured":"Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Hind M, Diwan A (eds) PLDI. ACM, pp 223\u2013234.","DOI":"10.1145\/1542476.1542501"},{"key":"209_CR78","volume-title":"Algorithms + data structures = programs","author":"N Wirth","year":"1978","unstructured":"Wirth N (1978) Algorithms + data structures = programs. Prentice-Hall Series in Automatic Computation, Pearson Education"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0209-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0209-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0209-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,10]],"date-time":"2019-08-10T12:35:29Z","timestamp":1565440529000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0209-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,21]]},"references-count":78,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["209"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0209-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5,21]]}}}