Testing a Saturation-Based Theorem Prover: Experiences and Challenges\n (Extended Version)

This paper attempts to address the question of how best to assure the\ncorrectness of saturation-based automated theorem provers using our experience\ndeveloping the theorem prover Vampire. We describe the techniques we currently\nemploy to ensure that Vampire is correct and use this to motivate future\nchallenges that need to be addressed to make this process more straightforward\nand to achieve better correctness guarantees.\n