Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423662 | Electronic Notes in Theoretical Computer Science | 2008 | 17 Pages |
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