E-matching for Fun and Profit
Michał Moskal, Jakub Łopuszański, Joseph R. Kiniry · Electronic Notes in Theoretical Computer Science · 2008
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.