Efficient E-Matching for SMT Solvers
From MaRDI portal
Publication:3608773
Recommendations
Cited in
(65)- A learning-based approach to synthesizing invariants for incomplete verification engines
- The QSMA algorithm for quantifiers in SMT
- 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
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Schemata of SMT-problems
- 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
- Towards satisfiability modulo parametric bit-vectors
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
- 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
- Array theory of bounded elements and its applications
- Fault-tolerant aggregate signatures
- 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
- Congruence closure with free variables
- 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
- A formal model to prove instantiation termination for E-matching-based axiomatisations
- Rocket-Fast Proof Checking for SMT Solvers
- DKAL and Z3: a logic embedding experiment
- Efficiently solving quantified bit-vector formulas
- Deciding local theory extensions via E-matching
- Solving quantified bit-vector formulas using binary decision diagrams
- Correct code containing containers
- E-matching with free variables
- Introducing robust reachability
- Finding connections via satisfiability solving
- Satisfiability modulo theories
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Linear Arithmetic with Stars
- Cazamariposas: automated instability debugging in SMT-based program verification
- Towards bit-width-independent proofs in SMT solvers
- 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
- 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
- A decision procedure for (co)datatypes in SMT solvers
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- Multi-prover verification of floating-point programs
- E-matching for fun and profit
- Satisfiability solving and model generation for quantified first-order logic formulas
- Model finding for recursive functions in SMT
- SAT-Inspired Eliminations for Superposition
- ALASCA: reasoning in quantified linear arithmetic
- Incremental dead state detection in logarithmic time
- Early verification of legal compliance via bounded satisfiability checking
- Light-weight SMT-based model checking
- AUTO2, a saturation-based heuristic prover for higher-order logic
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
- Constraint solving for finite model finding in SMT solvers
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)
