Article ID Journal Published Year Pages File Type
423662 Electronic Notes in Theoretical Computer Science 2008 17 Pages PDF
Abstract

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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics