{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T12:20:19Z","timestamp":1778588419138,"version":"3.51.4"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T00:00:00Z","timestamp":1501718400000},"content-version":"unspecified","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":[[2017,12]]},"DOI":"10.1007\/s10703-017-0290-y","type":"journal-article","created":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T09:58:16Z","timestamp":1501754296000},"page":"500-532","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Solving quantified linear arithmetic by counterexample-guided instantiation"],"prefix":"10.1007","volume":"51","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"King","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,3]]},"reference":[{"key":"290_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bodik R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2014) Syntax-guided synthesis. To Appear in Marktoberdorf NATO proceedings","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"290_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Fisman D, Singh R, Solar-Lezama A (2016) Results and analysis of sygus-comp\u201915. arXiv preprint arXiv:1602.01170","DOI":"10.4204\/EPTCS.202.3"},{"key":"290_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Radhakrishna A, Udupa A (2016) Scaling enumerative program synthesis via divide and conquer. Technical report, UPenn https:\/\/www.seas.upenn.edu\/~arjunrad\/publications\/eusolver_report.pdf","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"290_CR4","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0743-1066(95)00033-G","volume":"24","author":"R Backofen","year":"1995","unstructured":"Backofen R (1995) A complete axiomatization of a theory with feature and arity constraints. J Log Program 24:37\u201372","journal-title":"J Log Program"},{"key":"290_CR5","doi-asserted-by":"crossref","unstructured":"Bansal K, Reynolds A, King T, Barrett C, Wies T (2015) Deciding local theory extensions via e-matching. In: Computer aided verification (CAV), Springer","DOI":"10.1007\/978-3-319-21668-3_6"},{"key":"290_CR6","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway C, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) Cvx4. In: Computer aided verification (CAV), Springer","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"290_CR7","unstructured":"Barrett C, Stump A, Tinelli C (2010) The satisfiability modulo theories library (SMT-LIB). http:\/\/www.SMT-LIB.org"},{"key":"290_CR8","doi-asserted-by":"crossref","unstructured":"Baumgartner P (2015) Smttotptp a converter for theorem proving formats. In: CADE-25, Lecture notes in computer science, vol 9195. Springer","DOI":"10.1007\/978-3-319-21401-6_19"},{"issue":"1","key":"290_CR9","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L Berman","year":"1980","unstructured":"Berman L (1980) The complexity of logical theories. Theor Comput Sci 11(1):71\u201377","journal-title":"Theor Comput Sci"},{"key":"290_CR10","doi-asserted-by":"crossref","unstructured":"Beyene TA, Chaudhuri S, Popeea C, Rybalchenko A (2014) A constraint-based approach to solving games on infinite graphs. In: POPL, pp 221\u2013234","DOI":"10.1145\/2535838.2535860"},{"key":"290_CR11","doi-asserted-by":"crossref","unstructured":"Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAV, pp 869\u2013882","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"290_CR12","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N (2010) Linear quantifier elimination as an abstract decision procedure. In Giesl J, H\u00e4hnle R (eds) IJCAR, LNCS, vol 6173. Springer, pp 316\u2013330","DOI":"10.1007\/978-3-642-14203-1_27"},{"key":"290_CR13","unstructured":"Bj\u00f8rner N, Janota M (2015) Playing with quantified satisfaction. In: 20th international conferences on logic for programming, artificial intelligence and reasoning\u2014short presentations, LPAR 2015, Suva, Fiji, 24\u201328 November 2015, pp 15\u201327"},{"key":"290_CR14","unstructured":"Bj\u00f8rner N, McMillan KL, Rybalchenko A (2012) Program verification as satisfiability modulo theories. In: SMT@IJCAR, pp 3\u201311"},{"issue":"2","key":"290_CR15","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H Comon","year":"1994","unstructured":"Comon H, Delor C (1994) Equational formulae with membership constraints. Inf Comput 112(2):167\u2013216","journal-title":"Inf Comput"},{"key":"290_CR16","first-page":"91","volume-title":"Machine intelligence","author":"DC Cooper","year":"1972","unstructured":"Cooper DC (1972) Theorem proving in arithmetic without multiplication. In: Meltzer B, Michie D (eds) Machine intelligence, vol 7. Edinburgh University Press, Edinburgh, pp 91\u2013100"},{"key":"290_CR17","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2007) Efficient e-matching for SMT solvers. In: Pfenning F, (ed) CADE, LNCS, vol 4603. Springer, pp 183\u2013198","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"290_CR18","unstructured":"Detlefs D, Nelson G, Saxe JB (2003) Simplify: a theorem prover for program checking. J. ACM, Technical report"},{"key":"290_CR19","unstructured":"Dutertre B (2015) Solving exists\/forall problems with yices. In: Workshop on Satisfiability modulo theories"},{"key":"290_CR20","unstructured":"Farzan A Kincaid Z (2016) Linear arithmetic satisfiability via strategy improvement. In: Proceedings of the twenty-fifth international joint conference on artificial intelligence, IJCAI 2016, New York, NY, USA, 9\u201315 July 2016, pp 735\u2013743"},{"key":"290_CR21","doi-asserted-by":"crossref","unstructured":"Fedyukovich G, Gurfinkel A, Sharygina N (2015) Automated discovery of simulation between programs. In: Logic for programming, artificial intelligence, and reasoning\u201420th international conference, LPAR-20 2015, Suva, Fiji, 24\u201328 November 2015, Proceedings, pp 606\u2013621","DOI":"10.1007\/978-3-662-48899-7_42"},{"key":"290_CR22","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S Feferman","year":"1959","unstructured":"Feferman S, Vaught RL (1959) The first order properties of products of algebraic systems. Fundam Math 47:57\u2013103","journal-title":"Fundam Math"},{"key":"290_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The computational complexity of logical theories, lecture notes in mathematics","author":"J Ferrante","year":"1979","unstructured":"Ferrante J, Rackoff CW (1979) The computational complexity of logical theories, lecture notes in mathematics, vol 718. Springer, Berlin"},{"key":"290_CR24","doi-asserted-by":"crossref","unstructured":"Ganzinger H, Korovin K (2003) New directions in instantiation-based theorem proving. In: Logic in computer science, 2003. IEEE","DOI":"10.1109\/LICS.2003.1210045"},{"key":"290_CR25","doi-asserted-by":"crossref","unstructured":"Ge Y, Barrett C, Tinelli C (2007) Solving quantified verification conditions using satisfiability modulo theories. In CADE, LNCS, vol 4603. Springer","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"290_CR26","doi-asserted-by":"crossref","unstructured":"Ge Y, de\u00a0Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Proceedings of CAV\u201909, LNCS, vol 5643. Springer","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"290_CR27","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI, pp 405\u2013416","DOI":"10.1145\/2254064.2254112"},{"key":"290_CR28","doi-asserted-by":"crossref","unstructured":"Heizmann M, Dietsch D, Leike J, Musa B, Podelski A (2015) Ultimate automizer with array interpolation. In: TACAS","DOI":"10.1007\/978-3-662-46681-0_43"},{"key":"290_CR29","volume-title":"Model Theory, encyclopedia of mathematics and its applications","author":"W Hodges","year":"1993","unstructured":"Hodges W (1993) Model Theory, encyclopedia of mathematics and its applications, vol 42. Cambridge University Press, Cambridge"},{"key":"290_CR30","doi-asserted-by":"crossref","unstructured":"Jacobs S (2009) Incremental instance generation in local reasoning. In: CAV \u201909, Springer, Berlin, Heidelberg, pp 368\u2013382","DOI":"10.1007\/978-3-642-02658-4_29"},{"key":"290_CR31","doi-asserted-by":"crossref","unstructured":"Janota M, Klieber W, Marques-Silva J, Clarke E (2012) Solving qbf with counterexample guided refinement. In: International conference on theory and applications of satisfiability testing, Springer, Berlin, Heidelberg, pp 114\u2013128","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"290_CR32","doi-asserted-by":"crossref","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification, Springer","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"290_CR33","volume-title":"Theory of computation","author":"D Kozen","year":"2006","unstructured":"Kozen D (2006) Theory of computation. Springer, Berlin"},{"key":"290_CR34","doi-asserted-by":"crossref","unstructured":"Kuncak V, Mayer M, Piskac R, Suter P (2010) Complete functional synthesis. In: Zorn BG, Aiken A (eds) PLDI. ACM, New york, pp 316\u2013329","DOI":"10.1145\/1806596.1806632"},{"key":"290_CR35","doi-asserted-by":"crossref","unstructured":"Kuncak V, Rinard M (2003) Structural subtyping of non-recursive types is decidable. In: Eighteenth annual IEEE symposium on logic in computer science (LICS). IEEE","DOI":"10.1109\/LICS.2003.1210049"},{"issue":"5","key":"290_CR36","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos R, Weispfenning V (1993) Applying linear quantifier elimination. Comput J 36(5):450\u2013462","journal-title":"Comput J"},{"key":"290_CR37","doi-asserted-by":"crossref","unstructured":"Lopes NP, Monteiro J (2014) Weakest precondition synthesis for compiler optimizations. In: VMCAI 2014, pp 203\u2013221","DOI":"10.1007\/978-3-642-54013-4_12"},{"key":"290_CR38","doi-asserted-by":"crossref","unstructured":"Maher MJ (1988) Complete axiomatizations of the algebras of the finite, rational, and infinite trees. In: IEEE symposium on logic in computer science","DOI":"10.1109\/LICS.1988.5132"},{"key":"290_CR39","volume-title":"The metamathematics of algebraic systems, studies in logic and the foundations of mathematics","author":"AI Mal\u2019cev","year":"1971","unstructured":"Mal\u2019cev AI (1971) The metamathematics of algebraic systems, studies in logic and the foundations of mathematics, vol 66. North-Holland, Amsterdam"},{"key":"290_CR40","doi-asserted-by":"crossref","unstructured":"Monniaux D (2009) Automatic modular abstractions for linear constraints. In: POPL 2009, pp 140\u2013151","DOI":"10.1145\/1594834.1480899"},{"key":"290_CR41","doi-asserted-by":"crossref","unstructured":"Monniaux D (2010) Quantifier elimination by lazy model enumeration. In: Touili T, Cook B, Jackson P, (eds), CAV, LNCS, vol 6174. Springer, pp 585\u2013599","DOI":"10.1007\/978-3-642-14295-6_51"},{"issue":"1","key":"290_CR42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2267454","volume":"17","author":"A Mostowski","year":"1952","unstructured":"Mostowski A (1952) On direct products of theories. J Symb Logic 17(1):1\u201331","journal-title":"J Symb Logic"},{"key":"290_CR43","doi-asserted-by":"crossref","unstructured":"Nipkow T (2008) Linear quantifier elimination. In: Automated reasoning, pp 18\u201333","DOI":"10.1007\/978-3-540-71070-7_3"},{"key":"290_CR44","unstructured":"Phan A, Bj\u00f8rner N, Monniaux D (2012) Anatomy of alternating quantifier satisfiability (work in progress). In SMT 2012"},{"key":"290_CR45","doi-asserted-by":"crossref","unstructured":"Platzer A, Quesel J-D, R\u00fcmmer P (2009) Real world verification. In: Automated Deduction\u2013CADE-22, Springer, Berlin, Heidelberg, pp 485\u2013501","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"290_CR46","unstructured":"Presburger M (1929) \u00fcber die vollst\u00e4ndigkeit eines gewissen systems der aritmethik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Comptes Rendus du premier Congr\u00e8s des Math\u00e9maticiens des Pays slaves, Warsawa, pp 92\u2013101"},{"key":"290_CR47","doi-asserted-by":"crossref","unstructured":"Pugh W (1991) The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: ACM\/IEEE conference supercomputing","DOI":"10.1145\/125826.125848"},{"key":"290_CR48","doi-asserted-by":"crossref","unstructured":"Reddy CR, Loveland DW (1978) Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, ACM Press, pp 320\u2013325","DOI":"10.1145\/800133.804361"},{"key":"290_CR49","doi-asserted-by":"crossref","unstructured":"Reger G, Suda M, Voronkov A (2015) Playing with avatar. In: Automated deduction-CADE-25, Springer, pp 399\u2013415","DOI":"10.1007\/978-3-319-21401-6_28"},{"key":"290_CR50","doi-asserted-by":"crossref","unstructured":"Reynolds A, Deters M, Kuncak V, Tinelli C, Barrett CW (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Computer aided verification \u201427th international conference, CAV 2015, San Francisco, CA, USA, 18-24 July 2015, Proceedings, Part II, pp 198\u2013216","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"290_CR51","doi-asserted-by":"crossref","unstructured":"Reynolds A, Tinelli C, Moura LD (2014) Finding conflicting instances of quantified formulas in SMT. In: Formal methods in computer-aided design (FMCAD)","DOI":"10.1109\/FMCAD.2014.6987613"},{"issue":"2","key":"290_CR52","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T Rybina","year":"2001","unstructured":"Rybina T, Voronkov A (2001) A decision procedure for term algebras with queues. ACM Trans Comput Logic (TOCL) 2(2):155\u2013181","journal-title":"ACM Trans Comput Logic (TOCL)"},{"key":"290_CR53","doi-asserted-by":"crossref","unstructured":"Saha S, Garg P, Madhusudan P (2015) Alchemist: learning guarded affine functions. In: Computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, 18\u201324 July 2015, Proceedings, Part I, pp 440\u2013446","DOI":"10.1007\/978-3-319-21690-4_26"},{"key":"290_CR54","doi-asserted-by":"crossref","unstructured":"Scholl C, Disch S, Pigorsch F, Kupferschmid S (2008) Using an smt solver and craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra. In: SMT, ACM, pp 18\u201326","DOI":"10.1145\/1512464.1512469"},{"key":"290_CR55","unstructured":"Skolem T (1919) Untersuchungen \u00fcber die Axiome des Klassenkalk\u00fcls and \u00fcber \u201cProduktations- und Summationsprobleme\u201d, welche gewisse Klassen von Aussagen betreffen. Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, no. 3, Oslo"},{"key":"290_CR56","doi-asserted-by":"crossref","unstructured":"Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: ISSAC 2011, pp 329\u2013336","DOI":"10.1145\/1993886.1993935"},{"key":"290_CR57","unstructured":"Sturm T, Weispfenning V (2002) Quantifier elimination in term algebras: the case of finite languages. TUM Muenchen, In: Computer algebra in scientific computing (CASC)"},{"issue":"4","key":"290_CR58","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe G (2009) The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J Autom Reason 43(4):337\u2013362","journal-title":"J Autom Reason"},{"issue":"2","key":"290_CR59","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe G (2016) The CADE ATP system competition\u2014CASC. AI Magazine 37(2):99\u2013101","journal-title":"AI Magazine"},{"issue":"1","key":"290_CR60","first-page":"64","volume":"55","author":"A Tarski","year":"1949","unstructured":"Tarski A (1949) Arithmetical classes and types of algebraically closed and real-closed fields. Bull Am Math Soc 55(1):64","journal-title":"Bull Am Math Soc"},{"issue":"64","key":"290_CR61","first-page":"1192","volume":"55","author":"A Tarski","year":"1949","unstructured":"Tarski A (1949) Arithmetical classes and types of boolean algebras. Bull Am Math Soc 55(64):1192","journal-title":"Bull Am Math Soc"},{"key":"290_CR62","volume-title":"Specifying syntactic structures","author":"R Treinen","year":"1997","unstructured":"Treinen R (1997) Feature trees over arbitrary structures, chapter 7. In: Blackburn P, de Rijke M (eds) Specifying syntactic structures. CSLI Publications and FoLLI, Stanford"},{"issue":"1\u20132","key":"290_CR63","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/S0304-3975(01)00185-2","volume":"275","author":"I Walukiewicz","year":"2002","unstructured":"Walukiewicz I (2002) Monadic second-order logic on tree-like structures. Theor Comput Sci 275(1\u20132):311\u2013346","journal-title":"Theor Comput Sci"},{"key":"290_CR64","doi-asserted-by":"crossref","unstructured":"Weispfenning V (1997) Complexity and uniformity of elimination in Presburger arithmetic. In: ISSAC \u201997, New York, NY, USA, ACM, pp 48\u201353","DOI":"10.1145\/258726.258746"},{"key":"290_CR65","doi-asserted-by":"crossref","unstructured":"Weispfenning V (1999) Mixed real-integer linear quantifier elimination. In: Proceedings of the 1999 international symposium on symbolic and algebraic computation, ISSAC \u201999, New York, NY, USA, ACM, pp 129\u2013136","DOI":"10.1145\/309831.309888"},{"issue":"1","key":"290_CR66","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger CM, Hamadi Y, De Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42(1):3\u201323","journal-title":"Form Methods Syst Des"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0290-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0290-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0290-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T20:29:22Z","timestamp":1569961762000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0290-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,3]]},"references-count":66,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["290"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0290-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,3]]}}}