Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
G. Reger, M. Suda, A. Voronkov:
"Testing a Saturation-Based Theorem Prover: Experiences and Challenges";
Vortrag: TAP 2017 - 11th International Conference on Tests & Proofs,
Marburg, Germany;
19.07.2017
- 20.07.2017; in: "Tests and Proofs - 11th International Conference, TAP 2017, Held as Part of STAF 2017, Marburg, Germany, July 19-20, 2017, Proceedings",
Springer,
10375 / Lecture Notes in Computer Science
(2017),
ISBN: 978-3-319-61466-3;
S. 152
- 161.
Kurzfassung englisch:
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience with developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.
Schlagworte:
theorem proving, proof checking, proof certification
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-61467-0_10
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_264635.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.