Mathématiques, information scientifique, logiciel
Intitulé de l'offre
Internship - Formal Semantics of the Specification Language ACSL H / F
Sujet de stage
Our team develops Frama-C, a code analysis platform for C programs which provides several analyzers as plug-ins. Frama-C allows the user to annotate C programs with formal specifications written in the ACSL specification language.
Frama-C can then ensure that a C program satisfies its formal specification by relying on several techniques, notably abstract interpretation (plug-in Eva), weakest preconditions calculus (plug-in Wp), and runtime verification (plug-in E-ACSL).
Yet, the soundness of the verification process assumes that every plug-in shares a common semantics of ACSL. Currently, this semantics is only described in natural language.
It leads to several inconsistencies and incorrectness that already occurred these last years. This internship, possibly followed by a PhD thesis, aims at fixing these issues by providing a formal semantics for (a subset of) ACSL.
Durée du contrat (en mois)
Description de l'offre
The formal semantics will be defined with respect to an existing formal semantics of the
C programming language, expanding upon the work done by Paolo Herms in his PhD thesis on the implementation of a certified verification condition generator.
Ideas could also come from similar works for other specification languages such as JML. The internship will focus on key constructs of ACSL, such as assertions and function contracts containing integer and pointer arithmetics, as well as memory-related predicates in order to define their formal semantics in one proof environment such as Coq.
The intern will also propose and implement a methodology for validating existing verification tools based on ACSL (such as the Frama-C plug-ins Wp, Eva, and E-ACSL) with respect to the defined formal semantics.
Following-up by a PhD thesis on the same topic is much welcome!
Knowledge in the following field is required :
Knowledge in the following fields is welcome :