Why3 and Proving A* Automatically
A Case Study of Why3 as a Tool for Automated Software Verification
K.M. Neumann (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
K.F. Wullaert – 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 verification of software can provide a more rigorous guarantee of correctness compared to conventional software testing methods. However, doing this by hand requires substantial effort and is often impractical. To combat this, various verification tools have been developed in recent decades to at least partially automate this process. In this paper we explore Why3, a tool for deductive program verification, by implementing and verifying the A* algorithm. We find that Why3's expressive language allows for easy implementation and verification of A*. However, we also find that it has a significant learning curve and requires some knowledge on formal verification to use. In spite of this, we find it is a useful tool for automated verification.