### 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.

### License

BSD License

### Topics

- Computer science/Programming languages/Language definitions
- Computer science/Semantics and reasoning
- Tools

### Session Isabelle_C

- C_Lexer_Language
- C_Ast
- C_Environment
- C_Parser_Language
- C_Lexer_Annotation
- C_Parser_Annotation
- C_Eval
- C_Command
- C_Document
- C_Main
- C0
- C1
- C2
- C_paper
- C_Appendices
- README

## Cite

×

Isabelle_C-AFP

    @article{Isabelle_C-AFP,
      author  = {Frédéric Tuong and Burkhart Wolff},
      title   = {Isabelle/C},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Isabelle_C.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Dec 19, 2019 : Isabelle2019