This is a limited proof of concept to search for research data, not a production system.

Search the MIT Libraries

Title: AutoCorres 1.0

Type Software Greenaway, David, Lim, Japheth (2014): AutoCorres 1.0. Zenodo. Software. https://zenodo.org/record/13342

Authors: Greenaway, David (NICTA and University of New South Wales) ; Lim, Japheth (NICTA and University of New South Wales) ;

Links

Summary

AutoCorres is a tool for use with the Isabelle/HOL interactive theorem prover that attempts to simplify the verification of software programs written in the C programming language. In particular, it takes the output of Michael Norrish's C-to-Isabelle parser and abstracts it into a logical representation intended to be easier to manually verify properties about. This version of AutoCorres works with the Isabelle 2014 distribution.

The following papers are based on the work in this tool:

Don't sweat the small stuff: Formal verification of C code without the pain David Greenaway, Japheth Lim, June Andronick and Gerwin Klein Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014 Bridging the gap: Automatic verified abstraction of C David Greenaway, June Andronick and Gerwin Klein Proceedings of the 3rd International Conference on Interactive Theorem Proving, pp. 99-115, Princeton, New Jersey, August, 2012

AutoCorres itself is licensed under the BSD open source license, but the attached software release contains other software components under other licenses including the GPL and LGPL. License information for each component is clearly marked inside the software repository.

More information

  • DOI: 10.5281/zenodo.13342

Subjects

  • software verification, Isabelle/HOL, C verification

Dates

  • Publication date: 2014
  • Issued: December 16, 2014

Rights

  • info:eu-repo/semantics/openAccess Open Access

Much of the data past this point we don't have good examples of yet. Please share in #rdi slack if you have good examples for anything that appears below. Thanks!

Format

electronic resource

Relateditems

DescriptionItem typeRelationshipUri
IsSupplementTohttps://doi.org/10.1007/978-3-642-32347-8_8
IsSupplementTohttps://doi.org/10.1145/2594291.2594296
IsSupplementedByhttp://ssrg.nicta.com.au/projects/TS/autocorres/
IsPartOfhttps://zenodo.org/communities/zenodo