E-matching for fun and profit. (English) Zbl 1277.68142
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 19-35 (2008).
Summary: 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.
For the entire collection see [Zbl 1276.68020].
For the entire collection see [Zbl 1276.68020].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
References:
| [1] | Ball, T.; Lahiri, S. K.; Musuvathi, M., Zap: Automated theorem proving for software analysis, (Sutcliffe, G.; Voronkov, A., LPAR. LPAR, Lecture Notes in Computer Science, 3835 (2005)), 2-22 · Zbl 1143.68576 |
| [2] | Barnett, M.; Leino, K.; Schulte, W., The Spec# programming system: An overview, (Proceeding of CASSIS 2004. Proceeding of CASSIS 2004, LNCS, 3362 (2004)) |
| [3] | Barrett, C., L. de Moura and A. Stump, Design and Results of the 3rd Satisfiability Modulo Theories Competition (SMT-COMP 2007)http://www.smtcomp.org/2007/; Barrett, C., L. de Moura and A. Stump, Design and Results of the 3rd Satisfiability Modulo Theories Competition (SMT-COMP 2007)http://www.smtcomp.org/2007/ · Zbl 1129.68498 |
| [4] | Barrett, C.; Tinelli, C., CVC3, (Damm, W.; Hermanns, H., CAV. CAV, LNCS, 4590 (2007)), 298-302 |
| [5] | Conchon, S., E. Contejean, J. Kanig and S. Lescuyer, Lightweight Integration of the Ergo Theorem Prover inside a Proof AssistantSecond Automated Formal Methods workshop series (AFM07); Conchon, S., E. Contejean, J. Kanig and S. Lescuyer, Lightweight Integration of the Ergo Theorem Prover inside a Proof AssistantSecond Automated Formal Methods workshop series (AFM07) |
| [6] | de Moura, L. M.; Bjørner, N., Efficient E-matching for SMT solvers, (Pfenning, F., CADE. CADE, LNCS, 4603 (2007)), 183-198 · Zbl 1213.68578 |
| [7] | Detlefs, D., G. Nelson and J.B. Saxe, Simplify: A theorem prover for program checking; Detlefs, D., G. Nelson and J.B. Saxe, Simplify: A theorem prover for program checking · Zbl 1323.68462 |
| [8] | Dutertre, B.; de Moura, L. M., A fast linear-arithmetic solver for DPLL(T), (Ball, T.; Jones, R. B., CAV. CAV, LNCS, 4144 (2006)), 81-94 |
| [9] | Flanagan, C., R. Joshi and J.B. Saxe, An explicating theorem prover for quantified formulas; Flanagan, C., R. Joshi and J.B. Saxe, An explicating theorem prover for quantified formulas |
| [10] | Flanagan, C., K. Leino, M. Lillibridge, G. Nelson, J.B. Saxe and R. Stata, Extended static checking for JavaACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI’2002); Flanagan, C., K. Leino, M. Lillibridge, G. Nelson, J.B. Saxe and R. Stata, Extended static checking for JavaACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI’2002) |
| [11] | Kiniry, J. R.; Cok, D. R., ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system, (Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop. Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS 2004. Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop. Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS 2004, LNCS, 3362 (2005)) |
| [12] | Kozen, D., Complexity of finitely generated algebrasProceedings of the \(9^{th} \); Kozen, D., Complexity of finitely generated algebrasProceedings of the \(9^{th} \) |
| [13] | Moskal, M.; Skalski, K.; Olszta, P., Nemerle programming language |
| [14] | Nieuwenhuis, R.; Oliveras, A., Proof-Producing Congruence Closure, (Giesl, J., 16th International Conference on Term Rewriting and Applications, RTA’05. 16th International Conference on Term Rewriting and Applications, RTA’05, Lecture Notes in Computer Science, 3467 (2005)), 453-468 · Zbl 1078.68661 |
| [15] | Plotkin, G. D., Building-in equational theories, (Michie, D.; Meltzer, B., Machine Intelligence (1972)), 73-90 · Zbl 0262.68036 |
| [16] | Ramakrishnan, I. V.; Sekar, R. C.; Voronkov, A., Term indexing, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 1853-1964 · Zbl 0992.68189 |
| [17] | Ranise, S.; Tinelli, C., The Satisfiability Modulo Theories Library (SMT-LIB) (2007) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
