Solving quantified verification conditions using satisfiability modulo theories
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 2086596 (Why is no real title available?)
- Automated Reasoning
- Automated deduction by theory resolution
- Computer Aided Verification
- E-matching for fun and profit
- Efficient E-Matching for SMT Solvers
- Ordered semantic hyper-linking
- Partial instantiation methods for inference in first-order logic
- Simplify: a theorem prover for program checking
- Splitting on Demand in SAT Modulo Theories
- The TPTP problem library. CNF release v1. 2. 1
- The model evolution calculus as a first-order DPLL method
- Unification theory
Cited in
(30)- scientific article; zbMATH DE number 7333237 (Why is no real title available?)
- Syntax-guided quantifier instantiation
- Computer Aided Verification
- Triggerless happy. Intermediate verification with a first-order prover
- Back to the future, revisiting precise program verification using SMT solvers
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- Verification of SMT systems with quantifiers
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- An instantiation scheme for satisfiability modulo theories
- Bounded quantifier instantiation for checking inductive invariants
- Induction for SMT solvers
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Model generation for quantified formulas: a taint-based approach
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Congruence closure with free variables
- Quantifier instantiation techniques for finite model finding in SMT
- QMaude: quantitative specification and verification in rewriting logic
- Deciding local theory extensions via E-matching
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- versat: A Verified Modern SAT Solver
- An extension of lazy abstraction with interpolation for programs with arrays
- Invariant checking for SMT-based systems with quantifiers
- Revisiting enumerative instantiation
- Validating QBF Validity in HOL4
- Satisfiability solving and model generation for quantified first-order logic formulas
- Sharpening constraint programming approaches for bit-vector theory
- An interleaved depth-first search method for the linear optimization problem with disjunctive constraints
- Verifying Mixed Real-Integer Quantifier Elimination
- Constraint solving for finite model finding in SMT solvers
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)
