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

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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

License

BSD License

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