Solving quantified verification conditions using satisfiability modulo theories
DOI10.1007/S10472-009-9153-6zbMATH Open1184.68461OpenAlexW2009715851MaRDI QIDQ1037401FDOQ1037401
Authors: Yeting Ge, Clark Barrett, Cesare Tinelli 
Publication date: 16 November 2009
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-009-9153-6
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mechanization of proofs and logical operations (03B35)
Cites Work
- The TPTP problem library. CNF release v1. 2. 1
- Title not available (Why is that?)
- Simplify: a theorem prover for program checking
- Unification theory
- Splitting on Demand in SAT Modulo Theories
- Ordered semantic hyper-linking
- Automated deduction by theory resolution
- The model evolution calculus as a first-order DPLL method
- E-matching for fun and profit
- Efficient E-Matching for SMT Solvers
- Title not available (Why is that?)
- Computer Aided Verification
- Partial instantiation methods for inference in first-order logic
- Automated Reasoning
Cited In (30)
- Title not available (Why is that?)
- Computer Aided Verification
- Triggerless happy. Intermediate verification with a first-order prover
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Model generation for quantified formulas: a taint-based approach
- Validating QBF Validity in HOL4
- Syntax-guided quantifier instantiation
- An interleaved depth-first search method for the linear optimization problem with disjunctive constraints
- An instantiation scheme for satisfiability modulo theories
- Bounded quantifier instantiation for checking inductive invariants
- Congruence closure with free variables
- An extension of lazy abstraction with interpolation for programs with arrays
- Revisiting enumerative instantiation
- Deciding local theory extensions via E-matching
- Quantifier instantiation techniques for finite model finding in SMT
- Invariant checking for SMT-based systems with quantifiers
- Back to the future, revisiting precise program verification using SMT solvers
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- Solving quantified linear arithmetic by counterexample-guided instantiation
- QMaude: quantitative specification and verification in rewriting logic
- Verifying Mixed Real-Integer Quantifier Elimination
- Satisfiability solving and model generation for quantified first-order logic formulas
- Sharpening constraint programming approaches for bit-vector theory
- Verification of SMT systems with quantifiers
- Induction for SMT solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- versat: A Verified Modern SAT Solver
- Constraint solving for finite model finding in SMT solvers
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
Uses Software
This page was built for publication: Solving quantified verification conditions using satisfiability modulo theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1037401)
