A case study in formal verification of a Java program

TL;DR

This paper reports on the formal verification of a Java-based genetic algorithm, comparing tools and offering suggestions to improve usability and adoption of formal methods in software verification.

Contribution

It provides a case study on verifying Java code with Krakatoa and discusses usability enhancements for formal verification tools.

Findings

Krakatoa was identified as the most suitable tool for verifying the Java genetic algorithm.

The paper offers practical suggestions to improve formal verification tool usability.

It emphasizes the potential benefits of abduction capabilities in theorem provers.

Abstract

We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and select Krakatoa as the most appropriate for the task. Based on our experience, we present several suggestions for making the tools more user friendly, which we hope will lead to wider adoption of formal methods. In particular, we discuss at length how useful it would be for provers to perform some form of abduction, that is, for them to guess which extra assumptions they need to prove a statement. It is our opinion that progress in this area would produce the largest improvement in the usability of formal verification tools.