The University of New South Wales

AutoCorres: automatic specification abstraction

AutoCorres is a program verification tool developed at the Trustworthy Systems Group.

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.

Downloads

AutoCorres requires Isabelle 2020. The downloads below include a bundled copy of the C-to-Isabelle parser, which is also required for AutoCorres. The tool is released under a BSD-style license, however some bundled components are under other licenses. Please refer to copyright notices included in the release for further details.

Not using Isabelle2020? See our older releases.

Current release and documentation

Download AutoCorres 1.7 (Released 2020-11-02, Isabelle 2020)

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

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

Changelog

AutoCorres 1.7

AutoCorres 1.6.1

AutoCorres 1.6

AutoCorres 1.5

AutoCorres 1.4

AutoCorres 1.3

AutoCorres 1.2

AutoCorres 1.1

Development

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

Old releases

Publications

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

 

People

Past