Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
From MaRDI portal
Publication:3608772
Recommendations
Cited in
(43)- Solving quantified verification conditions using satisfiability modulo theories
- Theory decision by decomposition
- Solving quantified linear arithmetic by counterexample-guided instantiation
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Syntax-guided quantifier instantiation
- Making theory reasoning simpler
- Refutation-based synthesis in SMT
- Revisiting enumerative instantiation
- Array theory of bounded elements and its applications
- On interpolation in automated theorem proving
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Interpolation systems for ground proofs in automated deduction: a survey
- Adding decision procedures to SMT solvers using axioms with triggers
- Parametric quantified SAT solving
- Satisfiability solving and model generation for quantified first-order logic formulas
- Satisfiability modulo theories
- Congruence closure with free variables
- Linear Arithmetic with Stars
- Engineering DPLL(T) + Saturation
- Verifying Mixed Real-Integer Quantifier Elimination
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Incremental Instance Generation in Local Reasoning
- Combining theories with shared set operations
- On deciding satisfiability by theorem proving with speculative inferences
- scientific article; zbMATH DE number 1903356 (Why is no real title available?)
- Quantifier instantiation techniques for finite model finding in SMT
- Triggerless happy. Intermediate verification with a first-order prover
- Induction for SMT solvers
- Light-weight SMT-based model checking
- Model Evolution with Equality Modulo Built-in Theories
- Computer Aided Verification
- Automatic decidability and combinability
- scientific article; zbMATH DE number 7333237 (Why is no real title available?)
- Model generation for quantified formulas: a taint-based approach
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Verification of SMT systems with quantifiers
- QMaude: quantitative specification and verification in rewriting logic
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Early verification of legal compliance via bounded satisfiability checking
- The QSMA algorithm for quantifiers in SMT
- A formal model to prove instantiation termination for E-matching-based axiomatisations
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Quantifier simplification by unification in SMT
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 Q3608772)
