VanHelsing: A Fast Proof Checker for Debuggable Compiler Verification - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

VanHelsing: A Fast Proof Checker for Debuggable Compiler Verification

Résumé

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.
Fichier non déposé

Dates et versions

cea-01836303 , version 1 (12-07-2018)

Identifiants

Citer

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⟩
18 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More