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},
}
|