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