Theory Introduction_AutoCorres2

(*<*)

(*
 * Copyright (c) 2024 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Introduction_AutoCorres2
  imports Main

begin
(*>*)

chapter ‹Introduction›

text ‹
AutoCorres2 is a tool to facilitate the verification of C programs within Isabelle \<^cite>‹LNCS2283›.
It is a fork of AutoCorres: 🌐‹https://trustworthy.systems/projects/OLD/autocorres/›.
Here some quick links into the document:
▪ Quickstart guide for users (\autoref{chap:Quickstart}):
   🗏‹doc/quickstart/Chapter1_MinMax.thy›
▪ Background information, internals and some history of AutoCorres (\autoref{chap:AutoCorresInfrastructure}):
   🗏‹doc/AutoCorresInfrastructure.thy› 
▪ C-Parser
  ▪ Some internals (\autoref{chap:CTranslationInfrastructure}):
   🗏‹c-parser/CTranslationInfrastructure.thy› 
  ▪ Original documentation (outdated) (\autoref{chap:strictc}):
   The supported subset of C is extended. Moreover, the C-parser is integrated into Isabelle/ML and
   no standalone C-parser is supplied. The description of the design principles is
   still valid:
   🗏‹c-parser/doc/ctranslation_body.tex›
›

(*<*)
end
(*>*)

text_raw ‹\part{Library}›