Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda
Master Project of Olav de Haas

Abstract

Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof in the style of Hoare. This process has been mechanized by the introduction of Separation Logic and computer assisted verification tools. However, the tools fail to achieve the readability and convenience of manual paper proof outlines. This is a pity, because getting ideas and proofs across is essential for scientific research. I introduce a mechanization for proof outlines of imperative programs to interactively write human readable outlines in the dependently typed programming language and proof assistant Agda. I achieve this by introducing practical syntax and proof automation to write concise proof outlines for a simple imperative programming language based on λ-calculus. The proposed solution results in proof outlines that combine the readability of paper proof outlines and the precision of mechanization.

Thesis

• Haas, Olav de. Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda. TU Delft Repository, 2022.