# 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{https://isa-afp.org/entries/Isabelle_C.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License