AutoCorres2

Matthew Brecknell, David Greenaway, Johannes Hölzl 📧, Fabian Immler 📧, Gerwin Klein 📧, Rafal Kolanski 📧, Japheth Lim, Michael Norrish, Norbert Schirmer 📧, Salomon Sickert, Thomas Sewell, Harvey Tuch and Simon Wimmer

April 17, 2024

Abstract

AutoCorres2 is a tool to facilitate the verification of C programs within Isabelle. It is a fork of AutoCorres.

License

BSD License

History

February 18, 2025
Some support for post increment / decrement in expressions, anonymous structs and unions, flexible array members of structs.

Topics

Session AutoCorres2

Session AutoCorres2_Main

Session AutoCorres2_Test

Depends on

Cite

× 
@article{AutoCorres2-AFP,
  author  = {Matthew Brecknell and David Greenaway and Johannes Hölzl and Fabian Immler and Gerwin Klein and Rafal Kolanski and Japheth Lim and Michael Norrish and Norbert Schirmer and Salomon Sickert and Thomas Sewell and Harvey Tuch and Simon Wimmer},
  title   = {AutoCorres2},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/AutoCorres2.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: