E-matching for fun and profit

DOI10.1016/J.ENTCS.2008.04.078MaRDI QIDQ2864401zbMATH OpenOpenAlexFDO

Authors Michał Moskal, Jakub Łopuszański, Joseph R. Kiniry

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.04.078

zbMATH Keywords

SMTquantifier instantiationE-matching

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Recommendations

• Efficient E-Matching for SMT Solvers
• E-matching with free variables
• Deciding local theory extensions via E-matching
• Syntax-guided quantifier instantiation
• Satisfiability modulo theories: an appetizer

Cites work

• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
• Efficient E-Matching for SMT Solvers
• Simplify: a theorem prover for program checking
• Term Rewriting and Applications
• Term indexing
• Zap: Automated Theorem Proving for Software Analysis

Cited in

(10)

• Efficient E-Matching for SMT Solvers
• Profit-maximizing matchmaker
• Verifying visibility-based weak consistency
• Symbolic encoding of LL(1) parsing and its applications
• A heuristic prover for real inequalities
• Solving quantified verification conditions using satisfiability modulo theories
• E-matching with free variables
• Solving hard Mizar problems with instantiation and strategy invention
• Satisfiability solving and model generation for quantified first-order logic formulas
• Engineering DPLL(T) + Saturation

Describes a project that uses

Uses Software

• Nemerle
• ESC/Java
• Zap
• SIMPLIFY
• z3
• cvc3
• Spec#
• SMT-LIB

This page was built for publication: E-matching for fun and profit

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864401)