Exploring the Capabilities and Limitations of Algorithm Verification in Vampire
Case Studies in Verifying the Correctness of Selection Sort and of a Key-Value Store
M. Balfakeih (TU Delft - Electrical Engineering, Mathematics and Computer Science)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
M. Izadi – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Formal software verification is an important task for ensuring software correctness, especially in safety-critical systems. One method of formal verification is automated theorem proving, where one defines their program as a set of axioms and its correctness criteria as conjectures. We investigated the suitability of Vampire, an automated theorem prover, for formal verification by analyzing the logical foundations and performing case studies. In these case studies, we implemented Selection Sort and a Key-Value Store to observe what could be represented and proven. We were unable to prove the correctness of Selection Sort, but were able to prove most properties of a Key-Value Store. We discuss the capabilities and limitations of Vampire for formal software verification, namely that it is able to prove many properties of the functions we defined, unless they are heavily reliant on inductive definitions or too general with respect to the axioms. We believe that Vampire's inductive capabilities are currently insufficient for our use case. We reflect on the experience of using Vampire from the perspective of the average computer scientist and give suggestions for further documentation. We then discuss related work, including using Isabelle, another ATP and proof assistant, to reason about sorting algorithms and a Key-Value Store. Finally, we give suggestions for future work, such as rewriting the Key-Value Store in SMT-LIB, a language used as input for SMT solvers.