Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)
This addresses the reliability of theorem provers for formal verification and automated reasoning, but it is incremental as it builds on existing practices without introducing new methods.
The paper tackles the problem of ensuring correctness in saturation-based automated theorem provers, using the development of Vampire as a case study to describe current techniques and identify future challenges for improving correctness guarantees.
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience 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.