Isabelle/C

 

Title: Isabelle/C
Authors: Frédéric Tuong and Burkhart Wolff
Submission date: 2019-10-22
Abstract: We present a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various techniques such as deductive program verification or white-box testing can be applied to the same source, which is part of an integrated PIDE document model. Semantic back-ends are free to choose the supported C fragment and its semantics. In particular, they can differ on the chosen memory model or the specification mechanism for framing conditions. Our framework supports semantic annotations of C sources in the form of comments. Annotations serve to locally control back-end settings, and can express the term focus to which an annotation refers. Both the logical and the syntactic context are available when semantic annotations are evaluated. As a consequence, a formula in an annotation can refer both to HOL or C variables. Our approach demonstrates the degree of maturity and expressive power the Isabelle/PIDE sub-system has achieved in recent years. Our integration technique employs Lex and Yacc style grammars to ensure efficient deterministic parsing. This is the core-module of Isabelle/C; the AFP package for Clean and Clean_wrapper as well as AutoCorres and AutoCorres_wrapper (available via git) are applications of this front-end.
BibTeX:
@article{Isabelle_C-AFP,
  author  = {Frédéric Tuong and Burkhart Wolff},
  title   = {Isabelle/C},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/Isabelle_C.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License