Trustworthy Systems

AutoCorres: automatic specification abstraction

AutoCorres is a program verification tool developed at Trustworthy Systems.

Spec chain
C code is automatically abstracted into increasingly more abstract specifications, easing manual reasoning about the code.

AutoCorres (up to 1.0) was developed by David Greenaway. Most of its theories and algorithms are described in his PhD thesis.

Current release and documentation

See the AutoCorres GitHub relases for the latest version of AutoCorres and a bundled version of the C-to-Isabelle parser.

Quickstart Guide (PDF): A whirlwind introduction to AutoCorres.

The supplied README gives an overview of the available AutoCorres configuration options and example proofs.


See the latest change log on GitHub.


AutoCorres is developed as part of the L4.verified repository, in the tools/autocorres directory.


Abstract PDF David Greenaway
Automated proof-producing abstraction of c code
PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015
Abstract PDF David Greenaway, Japheth Lim, June Andronick and Gerwin Klein
Don't sweat the small stuff: Formal verification of C code without the pain
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014
Abstract PDF David Greenaway, June Andronick and Gerwin Klein
Bridging the gap: Automatic verified abstraction of C
International Conference on Interactive Theorem Proving, pp. 99–115, Princeton, New Jersey, USA, August, 2012