In short ...
Isabelle_C is 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 pro- gram 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 subsystem has achieved in recent years. Our integration technique employs Lex and Yacc style grammars to ensure efficient deterministic parsing. We present two case studies for the integration of (known) semantic back-ends in order to validate the design decisions for our back-end interface.
There is a ZENODO Page for an Isabelle_C bundle including AutoCorres
The Sources of Isabelle_C can be drawn from our GIT . Use the current C-2021-1 Branch.
Publications
- Frederic Tuong and Burkhart Wolff: Deeply Integrating C11 Code Support into Isabelle/PIDE. In International Workshop on Formal Integrated Development Environments (F-IDE 2019).
- Also presented at the Isabelle/Workshop 2020. Video Version.
- Frederic's Talk at Trinity College Dublin.
Tutorial
- General Introduction
- Getting Started (1) : The Global Architecture
- Getting Started (2) : Firing Up
- Getting Started (3) : Editing an arbitrary File
- Editing C in Isabelle_C : Basics
- Parsing Stress Tests in Isabelle_C : Comments and Directives
- Editing Stress-Test : The Ball, Editing Stress-Test : The Ball 17:45 - 18:20 (BAD)
- Editing Stress-Test : Obfuscated C
- Editing External C sources
- Tracing Bindings in Isabelle_C PIDE
- Annotation Commands
- Annotation Commands
- Annotation Commands
- Annotation Commands
- Annotation Commands
- Annotation Commands