Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
From MaRDI portal
Publication:3608772
DOI10.1007/978-3-540-73595-3_12zbMath1213.68376MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Light-Weight SMT-based Model Checking, Model Evolution with Equality Modulo Built-in Theories, Interpolation systems for ground proofs in automated deduction: a survey, Adding decision procedures to SMT solvers using axioms with triggers, On deciding satisfiability by theorem proving with speculative inferences, Automatic decidability and combinability, Quantifier simplification by unification in SMT, 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, Refutation-based synthesis in SMT, 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, Satisfiability Modulo Theories, Linear Arithmetic with Stars, Engineering DPLL(T) + Saturation, Combining Theories with Shared Set Operations
Uses Software
