Efficient E-Matching for SMT Solvers

DOI10.1007/978-3-540-73595-3_13zbMath1213.68578OpenAlexW1552077729MaRDI QIDQ3608773

Leonardo de Moura, Nikolaj Bjørner

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_13

Mathematics Subject Classification ID

Related Items (52)

A decision procedure for (co)datatypes in SMT solvers ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ A heuristic prover for real inequalities ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Quantifier simplification by unification in SMT ⋮ Not all bugs are created equal, but robust reachability can tell the difference ⋮ Satisfiability Modulo Theories ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Linear Arithmetic with Stars ⋮ An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ An instantiation scheme for satisfiability modulo theories ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Efficiently solving quantified bit-vector formulas ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Syntax-guided quantifier instantiation ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Congruence Closure with Free Variables ⋮ Schemata of SMT-Problems ⋮ Correct Code Containing Containers ⋮ Alloy*: a general-purpose higher-order relational constraint solver ⋮ DKAL and Z3: A Logic Embedding Experiment ⋮ Light-Weight SMT-based Model Checking ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ A formal methods approach to predicting new features of the eukaryotic vesicle traffic system ⋮ Formalization of the fundamental group in untyped set theory using auto2 ⋮ Refutation-based synthesis in SMT ⋮ Fault-Tolerant Aggregate Signatures ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ Rocket-Fast Proof Checking for SMT Solvers ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Model Finding for Recursive Functions in SMT ⋮ Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Extending SMT solvers to higher-order logic ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme ⋮ Theory decision by decomposition ⋮ E-matching for Fun and Profit ⋮ 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 ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• z3

This page was built for publication: Efficient E-Matching for SMT Solvers