Level: M1, M2
Contact: Burkhart Wolff
Summary. 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. The purpose of this stage is to develop a translation from C11-AST's generated in Isabelle/C to a semantic backend called AutoCorres, a complex execution model of the C ;language executed on ARM processors.
This ambitious project is actually a re-implementation and integration of existing prototypes: there is actually a Isabelle/C/AutoCorres version based on Isabelle2021 which is functional enough to serve as reference. However, AutoCorres exists meanwhile as a much more recent and self-contained AFP submission (see here), and the technologies inside Isabelle/C to compile the C11-AST's to a semantic backend have also dramatically improved. Since the long-term goal is a submission of Isabelle/C together with the AutoCorres backend, a re-implementation is necessary.
Read the detailed internship proposal.