VanHelsing: A Fast Proof Checker for Debuggable Compiler Verification

R. Lezuo 1 I. Dragan 1, 2 G. Barany 2, 1 A. Krall 1
1 Institute of Computer Languages
2 DILS - Département Ingénierie Logiciels et Systèmes
Abstract : In this paper we present vanHelsing, a fully automatic proof checker for a subset of first-order problemstailored to a class of problems that arise in compiler verification.vanHelsing accepts input problems formulated in a subset of theTPTP language and is optimized to efficiently solve expressionequivalence problems formulated in first-order logic. Being apractical tool vanHelsing provides also graphical debugging helpwhich makes the visualization of problems and localization offailed proofs much easier. The experimental evaluation showedthat this specialized tool performs up to a factor of 3 better thanstate of the art theorem provers.
Keywords : Computation theory Computer circuits Formal logic Open systems Problem solving Reconfigurable hardware Theorem proving Compiler verifications Expression equivalence First order logic Proof checkers Theorem provers Program compilers
Document type :
Conference papers
Complete list of metadatas
https://hal-cea.archives-ouvertes.fr/cea-01836303
Contributor : Léna Le Roy <>
Submitted on : Thursday, July 12, 2018 - 11:26:55 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Identifiers

Collections

CEA | CEA-UPSAY | DRT | LIST | UNIV-PARIS-SACLAY

Citation

R. Lezuo, I. Dragan, G. Barany, A. Krall. VanHelsing: A Fast Proof Checker for Debuggable Compiler Verification. 2015 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Sep 2015, Timisoara, Romania. pp.167-174, ⟨10.1109/SYNASC.2015.34⟩. ⟨cea-01836303⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

36

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD