CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Testing a saturation-based theorem prover: Experiences and challenges

Giles Reger ; Martin Suda ; Andrei Voronkov (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers))
Lecture Notes in Computer Science: 11th International Conference on Tests and Proofs, TAP 2017, held as part of STAF 2017; Marburg; Germany; 19 July 2017 through 20 July 2017 (03029743). Vol. 10375 LNCS (2017), p. 152-161.
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2017-10-02.
CPL Pubid: 252199

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)