[Zurück]

R Lezuo, I. Dragan, G. Barany, A. Krall:
"vanHelsing: A Fast Theorem Prover for Debuggable Compiler Verification";
Vortrag: 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2015), Timisoara; 21.09.2015 - 24.09.2015; in: "17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing", L. Kovacs, D. Zaharie (Hrg.); (2015), S. 167 - 174.

In this paper we present vanHelsing, a fully auto- matic first-order theorem prover aimed especially at the class of problems that arise in compiler verification. vanHelsing accepts input problems formulated in a subset of the TPTP language and is specially tailored to efficiently solve expression equivalence problems formulated in first-order logic. Besides solving these problems, vanHelsing provides also graphical debugging help which makes the visualization of problems and localization of failed proofs much easier. From our experiments we noticed that using this specialized tool one can gain up to factor 3 in performance when compared to the non-specific theorem provers.

theorem prover, compiler verification

http://dx.doi.org/10.1109/SYNASC.2015.34

http://publik.tuwien.ac.at/files/publik_247827.pdf