Integrating Rukia-Random-Testing in Isabelle/C

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.

[ MORE TO COME ON RUKIA AND RANDOM TESTING ]

Proceeding

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.

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, 2019-21.

Required Skills

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