Talks and Poster Presentations (with Proceedings-Entry):
R Lezuo, I. Dragan, G. Barany, A. Krall:
"vanHelsing: A Fast Theorem Prover for Debuggable Compiler Verification";
Talk: 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2015),
- 2015-09-24; in: "17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing",
L. Kovacs, D. Zaharie (ed.);
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
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.