Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
From MaRDI portal
Publication:3636870
DOI10.1007/978-3-642-02658-4_25zbMath1242.68280OpenAlexW1536511644MaRDI QIDQ3636870
Publication date: 30 June 2009
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02658-4_25
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (50)
A decision procedure for (co)datatypes in SMT solvers ⋮ An approximation framework for solvers and decision procedures ⋮ Contract-based verification of MATLAB-style matrix programs ⋮ Decision procedures for flat array properties ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Quantifier simplification by unification in SMT ⋮ Not all bugs are created equal, but robust reachability can tell the difference ⋮ Satisfiability Modulo Theories ⋮ Automated reasoning with restricted intensional sets ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Fuzzy answer set computation via satisfiability modulo theories ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Unifying splitting ⋮ A solver for arrays with concatenation ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Modular instantiation schemes ⋮ An instantiation scheme for satisfiability modulo theories ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Efficiently solving quantified bit-vector formulas ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Syntax-guided quantifier instantiation ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ Counterexample-Guided Model Synthesis ⋮ Congruence Closure with Free Variables ⋮ Schemata of SMT-Problems ⋮ Automatically inferring loop invariants via algorithmic learning ⋮ Alloy*: a general-purpose higher-order relational constraint solver ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ Refutation-based synthesis in SMT ⋮ CoReS: a tool for computing core graphs via SAT/SMT solvers ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Fault-Tolerant Aggregate Signatures ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ Towards Complete Reasoning about Axiomatic Specifications ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Model Finding for Recursive Functions in SMT ⋮ A unifying splitting framework ⋮ Extending SMT solvers to higher-order logic ⋮ Temporal prophecy for proving temporal properties of infinite-state systems ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Verifying Whiley programs with Boogie ⋮ Array theory of bounded elements and its applications ⋮ On interpolation in automated theorem proving ⋮ MedleySolver: online SMT algorithm selection
Uses Software
This page was built for publication: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
