Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda

Olav de Haas


Date: Mon, July 11, 2022
Time: 09:00
Room: Snijderszaal (building 36)
Note: This is a MSc thesis defense


Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof. 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. We 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. We 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.

Previous: |
Next: |