Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
From MaRDI portal
Publication:3608772
DOI10.1007/978-3-540-73595-3_12zbMATH Open1213.68376OpenAlexW1569747018MaRDI QIDQ3608772FDOQ3608772
Yeting Ge, Clark Barrett, Cesare Tinelli
Publication date: 6 March 2009
Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_12
Recommendations
Cited In (32)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer Aided Verification
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Quantifier simplification by unification in SMT
- Model generation for quantified formulas: a taint-based approach
- Incremental Instance Generation in Local Reasoning
- Syntax-guided quantifier instantiation
- Array theory of bounded elements and its applications
- Interpolation systems for ground proofs in automated deduction: a survey
- Adding decision procedures to SMT solvers using axioms with triggers
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- On deciding satisfiability by theorem proving with speculative inferences
- Automatic decidability and combinability
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Refutation-based synthesis in SMT
- Theory decision by decomposition
- Light-Weight SMT-based Model Checking
- Combining theories with shared set operations
- Linear Arithmetic with Stars
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- 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
- Model Evolution with Equality Modulo Built-in Theories
- Verifying Mixed Real-Integer Quantifier Elimination
- Verification of SMT systems with quantifiers
- Early verification of legal compliance via bounded satisfiability checking
- Satisfiability Modulo Theories
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Engineering DPLL(T) + Saturation
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 Q3608772)
