Solving Quantified Verification Conditions Using Satisfiability Modulo Theories

DOI10.1007/978-3-540-73595-3_12zbMath1213.68376OpenAlexW1569747018MaRDI QIDQ3608772

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

Mathematics Subject Classification ID

Related Items (19)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Quantifier simplification by unification in SMT ⋮ Synthesis of positive logic programs for checking a class of definitions with infinite quantification ⋮ Satisfiability Modulo Theories ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Linear Arithmetic with Stars ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Engineering DPLL(T) + Saturation ⋮ Syntax-guided quantifier instantiation ⋮ Automatic decidability and combinability ⋮ Light-Weight SMT-based Model Checking ⋮ Refutation-based synthesis in SMT ⋮ Model Evolution with Equality Modulo Built-in Theories ⋮ Combining Theories with Shared Set Operations ⋮ Theory decision by decomposition ⋮ Array theory of bounded elements and its applications ⋮ On interpolation in automated theorem proving

Uses Software

• cvc3

This page was built for publication: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories