Skip to main content

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.
  • Aim: Simplify formal verification of C code by automatically and provably abstracting low-level C semantics into higher-level representations.

  • Overview: AutoCorres is an automatic abstraction tool that can be used in conjunction with our C-to-Isabelle parser.

    The C parser translates C code into the logic of the Isabelle/HOL theorem prover. A delicate choice must be made when designing such a translator. On one hand, it is desirable to make the translator as simple as possible: if the translator incorrectly imports source code into logic, than proofs carried out on the imported program may not apply to the actual source code. On the other hand, the translated source code will need to be later manually reasoned about: if the translator only provides a primitive translation of source code, later reasoning will be cumbersome and time-consuming.

    AutoCorres automatically abstracts low-level translated programs into a form better suited for human reasoning. This allows the translation from source code into logic to remain simple (allowing users to have confidence in the translation) while still allowing program verifiers to work with a higher-level specification of the source code. This tool generates a proof of correspondence between the generated high-level specification and the input low-level specification, so users can be confident in the results.

  • Results:

    • AutoCorres can automatically and provably convert C programs into a higher-level monadic representation.
    • AutoCorres' heap abstraction feature allows users to carry out high-level reasoning about memory for type-safe functions, while still allowing byte-level reasoning where necessary.
    • AutoCorres' word abstraction feature can automatically and soundly abstract two's-complement machine words into unbounded natural numbers and integers, simplifying reasoning.
    • AutoCorres can be used to reason about non-trivial programs: it can parse the seL4 microkernel source code, for example.
    • AutoCorres allows high-level reasoning: an existing proof of the Schorr-Waite algorithm based on a highly-abstract machine could be ported to the output of AutoCorres on a concrete C implementation with minimal effort.
    • AutoCorres generates a proof of correctness in Isabelle/HOL for all of its translations. This means that you don't need to trust AutoCorres to soundly reason about its output.

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


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.


AutoCorres 1.7

  • Isabelle2020 edition of both AutoCorres and the C parser.
  • Slight updates to wp: use "wp (once)" instead of "wp_once".

AutoCorres 1.6.1

  • Correct license for a C parser file. No code changes.

AutoCorres 1.6

  • Isabelle2019 edition of both AutoCorres and the C parser.
  • Word abstraction has been extended to C bitwise operators.

AutoCorres 1.5

  • Isabelle2018 edition of both AutoCorres and the C parser.

AutoCorres 1.4

  • Isabelle2017 edition of both AutoCorres and the C parser.

AutoCorres 1.3

  • Isabelle2016-1 edition of both AutoCorres and the C parser.
  • AutoCorres and the C parser now support multiple architectures, and require the L4V_ARCH environment variable to be set according to your choice of architecture. See the README for details.

AutoCorres 1.2

  • Isabelle2016 edition of both AutoCorres and the C parser.
  • Incompatibility: functions excluded using the “scope” option are no longer translated to “fail”. Instead, they are translated to a wrapper around the C parser's specs. This makes it possible to do proofs on “scope”-limited AutoCorres specs.

AutoCorres 1.1

  • Isabelle2015 edition of both AutoCorres and the C parser.
  • New options for changing how AutoCorres names functions and globals.
  • Incompatibility: names of global variables have changed. Names have changed from “lifted_globals.foo_'” to “lifted_globals.foo_''”. Recover the old behaviour by setting lifted_globals_field_suffix="_'".
  • Minor incompatibility: intermediate function names have changed. They are now “l1_foo'”, “l2_foo'”... instead of “l1_foo”, “l2_foo”.
  • Renamed “ccorres” predicate to “ac_corres” for clarity.


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

Old releases


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




  • David Greenaway
  • Japheth Lim
  • June Andronick
  • Rohan Ben Jacob Rao