Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda

Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda

de Haas, Olav (TU Delft Electrical Engineering, Mathematics and Computer Science)

van Deursen, A. (graduation committee)
Krebbers, R.J. (graduation committee)
Cockx, J.G.H. (graduation committee)
Rouvoet, A.J. (mentor)

Delft University of Technology

Computer Science

2022-07-11

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.

Programming Languages
Proof assistant
Separation Logic
Formal Verification
Proof Automation
Agda

http://resolver.tudelft.nl/uuid:5ca6e6f3-1242-4b86-8307-4ac4f4489951

Implementation in Agda can be found at: https://github.com/Olavhaasie/hoare-proof-outlines

Student theses

master thesis

© 2022 Olav de Haas