Solving quantified linear arithmetic by counterexample-guided instantiation
From MaRDI portal
Recommendations
- Solving quantified verification conditions using satisfiability modulo theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
- Linear quantifier elimination as an abstract decision procedure
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
Cites work
- scientific article; zbMATH DE number 53151 (Why is no real title available?)
- scientific article; zbMATH DE number 1253963 (Why is no real title available?)
- scientific article; zbMATH DE number 2090860 (Why is no real title available?)
- scientific article; zbMATH DE number 3408928 (Why is no real title available?)
- A complete axiomatization of a theory with feature and arity constraints
- A constraint-based approach to solving games on infinite graphs
- A decision procedure for term algebras with queues
- Applying Linear Quantifier Elimination
- Automated discovery of simulation between programs
- Automatic modular abstractions for linear constraints
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computer Science Logic
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Deciding local theory extensions via E-matching
- Efficient E-Matching for SMT Solvers
- Efficiently solving quantified bit-vector formulas
- Equational formulae with membership constraints
- Incremental Instance Generation in Local Reasoning
- Linear Quantifier Elimination
- Linear quantifier elimination as an abstract decision procedure
- Monadic second-order logic on tree-like structures
- On direct products of theories
- Playing with AVATAR
- Presburger arithmetic with bounded quantifier alternation
- Real World Verification
- SMT-based model checking for recursive programs
- SMTtoTPTP -- a converter for theorem proving formats
- Scaling enumerative program synthesis via divide and conquer
- Simplify: a theorem prover for program checking
- Solving QBF with counterexample guided refinement
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- The CADE-14 ATP system competition
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- The complexity of logical theories
- The computational complexity of logical theories
- The first order properties of products of algebraic systems
- Theory of computation.
- Verification and synthesis using real quantifier elimination
- Weakest precondition synthesis for compiler optimizations
Cited in
(12)- Synthesising programs with non-trivial constants
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Syntax-guided quantifier instantiation
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- On solving quantified bit-vector constraints using invertibility conditions
- Refutation-based synthesis in SMT
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Solving hard Mizar problems with instantiation and strategy invention
- A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
- Linear quantifier elimination as an abstract decision procedure
- ALASCA: reasoning in quantified linear arithmetic
- Induction for SMT solvers
Describes a project that uses
Uses Software
This page was built for publication: Solving quantified linear arithmetic by counterexample-guided instantiation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688537)
