LMF
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
StageIsabelleCClean

Connecting Isabelle/C with Isabelle/Clean

Description

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 program verification or whitebox testing can be applied to the same source, which is part of an integrated Isabelle/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. Isabelle/C 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.

Clean is based on a simple execution model for an imperative target language. It strives for a type-safe notion of program-variables, an incremental construction of the typed state-space, support of incremental verification, and open-world extensibility of new type definitions being intertwined with the program definitions. Clean offers conditionals and loops supporting C-like control-flow operators such as break and return. Direct recursion of procedures is also supported. Clean’s design strives for extreme simplicity. It is geared towards symbolic execution and proven correct verification tools. Isabelle/Clean [2] provides the underlying libraries of this package.

Isabelle/Clean is intended to serve as demonstrator semantic backend for Isabelle/C, or for the test-generation techniques. The purpose of this stage is to write a translation --- based on existing infrastructure --- from the C11-AST's generated inside Isabelle/C to the lambda-terms underlying the Isabelle/Clean representation, thus using Isabelle/Clean as a semantic backend of Isabelle/C.

Work Plan

Implementing for each syntactic category in the C11 AST's via C11 library-routines a translation to the individual programming constructs supported by Clean. The implementation language is SML directly supported in the Isabelle programming environment. SML pattern-matching and various SML libraries will help at the task.

Required Skills

  • good functional programming skills
  • interest in compiler construction
  • no knowledge in theorem proving necessary

Bibliography

[1] Frédéric Tuong and Burkhart Wolff: 

    Deeply Integrating C11 Code Support into Isabelle/PIDE, FiDE, 2019.

[2] Frédéric Tuong and Burkhart Wolff: 

    The Isabelle/Clean Theory, 2019-21.

[3] Frederic Tuong and Burkhart Wolff: 

    Isabelle/C