Email Gateway (Aug 22 2022 at 21:10): Email Gateway (Aug 22 2022 at 21:10):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
https://www.isa-afp.org/entries/Isabelle_C.html
Isabelle/C
by Frédéric Tuong and Burkhart Wolff
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.
Enjoy!
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC