AutoCorres is a tool which can automatically produce a monadic abstraction of a C program, together with an Isabelle/HOL proof of correspondence between the abstraction and a low-level embedding of the C program. AutoCorres was developed primarily by David Greenaway during his PhD at NICTA and UNSW.
AutoCorres is currently distributed in the tools directory of the l4v verifcation of the seL4 microkernel.
This repository contains a couple of example proofs using AutoCorres, which I reworked for my own educational purposes.