E-matching for Fun and Profit

Efficient handling of quantifiers is crucial for solving software verification problems. E-matching algorithms are used in satisfiability modulo theories solvers that handle quantified formulas through instantiation. Two novel, efficient algorithms for solving the E-matching problem are presented and compared to a well-known algorithm described in the literature.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Michal Moskal, Jakub Lopuszanski, Joseph R. Kiniry
• Keywords: Algorithm, ENTCS 2008, Satisfiability Modulo Theories, Software Verification Problems