E-matching for Fun and Profit

DOI10.1016/j.entcs.2008.04.078zbMath1277.68142OpenAlexW2114917372MaRDI QIDQ2864401

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

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)

Related Items

Verifying Visibility-Based Weak Consistency, A heuristic prover for real inequalities, Symbolic encoding of LL(1) parsing and its applications, Engineering DPLL(T) + Saturation, Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas, Solving quantified verification conditions using satisfiability modulo theories

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Zap: Automated Theorem Proving for Software Analysis
• Term Rewriting and Applications