Efficient verification of imperative programs using auto2

TL;DR

This paper demonstrates how the auto2 prover in Isabelle can be effectively used to verify complex imperative programs and data structures through a modular and efficient approach.

Contribution

It introduces a novel framework applying auto2 to verify imperative programs, including data structures and algorithms, within Isabelle proof assistant.

Findings

Verified complex data structures like red-black trees and union-find.

Achieved efficient and modular verification of algorithms.

Demonstrated the applicability of auto2 for imperative program verification.

Abstract

Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the setup of auto2 for both stages of the proof process: verification of a functional version of the program, and refining to the imperative version using separation logic. As examples, we verify several data structures, including red-black trees, interval trees, priority queues, and union-find. We also verify several algorithms making use of these data structures. These examples show that our framework is able to verify complex algorithms efficiently and in a modular manner.