Solving quantified linear arithmetic by counterexample-guided instantiation
From MaRDI portal
Publication:1688537
DOI10.1007/s10703-017-0290-yzbMath1377.68138OpenAlexW2744775619WikidataQ124817119 ScholiaQ124817119MaRDI QIDQ1688537
Andrew Reynolds, Viktor Kuncak, Tim King
Publication date: 8 January 2018
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: http://infoscience.epfl.ch/record/255788
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
Synthesising programs with non-trivial constants ⋮ Syntax-guided quantifier instantiation ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Refutation-based synthesis in SMT ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- SMT-based model checking for recursive programs
- The complexity of logical theories
- The computational complexity of logical theories
- The CADE-14 ATP system competition
- Equational formulae with membership constraints
- Monadic second-order logic on tree-like structures
- Deciding local theory extensions via E-matching
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Efficiently solving quantified bit-vector formulas
- Theory of computation.
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Solving QBF with Counterexample Guided Refinement
- Weakest Precondition Synthesis for Compiler Optimizations
- A complete axiomatization of a theory with feature and arity constraints
- Applying Linear Quantifier Elimination
- A decision procedure for term algebras with queues
- The first order properties of products of algebraic systems
- Scaling Enumerative Program Synthesis via Divide and Conquer
- SMTtoTPTP – A Converter for Theorem Proving Formats
- Playing with AVATAR
- Automated Discovery of Simulation Between Programs
- Linear Quantifier Elimination
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Incremental Instance Generation in Local Reasoning
- Real World Verification
- Verification and synthesis using real quantifier elimination
- Automatic modular abstractions for linear constraints
- Computer Science Logic
- Presburger arithmetic with bounded quantifier alternation
- A constraint-based approach to solving games on infinite graphs
- Linear Quantifier Elimination as an Abstract Decision Procedure
- On direct products of theories
This page was built for publication: Solving quantified linear arithmetic by counterexample-guided instantiation
