Efficient E-Matching for SMT Solvers
From MaRDI portal
Publication:3608773
DOI10.1007/978-3-540-73595-3_13zbMATH Open1213.68578OpenAlexW1552077729MaRDI QIDQ3608773FDOQ3608773
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
Recommendations
Cited In (60)
- Introducing robust reachability
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Transforming optimization problems into disciplined convex programming form
- Invariant neural architecture for learning term synthesis in instantiation proving
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- ALASCA: reasoning in quantified linear arithmetic
- Incremental dead state detection in logarithmic time
- Early verification of legal compliance via bounded satisfiability checking
- A learning-based approach to synthesizing invariants for incomplete verification engines
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- Not all bugs are created equal, but robust reachability can tell the difference
- Quantifier simplification by unification in SMT
- Model Finding for Recursive Functions in SMT
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
- Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Alloy*: a general-purpose higher-order relational constraint solver
- Syntax-guided quantifier instantiation
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
- Towards satisfiability modulo parametric bit-vectors
- Array theory of bounded elements and its applications
- 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
- An instantiation scheme for satisfiability modulo theories
- 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 extension of lazy abstraction with interpolation for programs with arrays
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Refutation-based synthesis in SMT
- Solving quantified verification conditions using satisfiability modulo theories
- Theory decision by decomposition
- Rocket-Fast Proof Checking for SMT Solvers
- Schemata of SMT-Problems
- Fault-Tolerant Aggregate Signatures
- Efficiently solving quantified bit-vector formulas
- Multi-Prover Verification of Floating-Point Programs
- Light-Weight SMT-based Model Checking
- Congruence Closure with Free Variables
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Linear Arithmetic with Stars
- Formalization of the fundamental group in untyped set theory using auto2
- Towards bit-width-independent proofs in SMT solvers
- Extending SMT solvers to higher-order logic
- On interpolation in automated theorem proving
- A decision procedure for (co)datatypes in SMT solvers
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
- E-matching for fun and profit
- SAT-Inspired Eliminations for Superposition
- DKAL and Z3: A Logic Embedding Experiment
- Correct Code Containing Containers
- Satisfiability Modulo Theories
- A Decision Procedure for (Co)datatypes in SMT Solvers
- Constraint solving for finite model finding in SMT solvers
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
Uses Software
This page was built for publication: Efficient E-Matching for SMT Solvers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608773)
