6-month Master Internship on Formal Semantics of the Specification Language ACSL H/F (Mathématiques, information  scientifique, logiciel)

Job description

Domaine : Mathématiques, information  scientifique, logiciel

Contrat : Stage

Description du poste :

Our team develops Frama-C, an Open-Source code analysis platform for C programs which provides several collaborative 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 inter-
pretation (plug-in Eva), weakest preconditions calculus (plug-in Wp), and runtime verification (plug-in E-ACSL). Therefore, ACSL is the lingua franca shared by the Frama-C plug-ins. It is one of the key for plug-in collaborations. For instance, some ACSL properties may be proved by a plug-in A under a few hypotheses that are expressed as another set of ACSL properties that may in turn be proved by
another plug-in B. Yet, the soundness of the whole verification process assumes that every plug-in shares the same semantics of ACSL. Currently, this semantics is only described by the reference manual written in natural language (American English). It leads to several issues that already occurred these last years. For instance, the ACSL manual may contain partial definitions and/or insufficient explanations that open the door to inconsistent interpretations (by plug-in developers, or end-users). This internship, possibly followed by a PhD thesis on the same topic, aims at fixing these issues by defining a formal semantics for (a subset of) ACSL with respect to an existing formal semantics of the C programming language (e.g. CompCert memory model, the executable semantics formalized in the K framework, or Robbert Krebber's PhD thesis), 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.


Knowledge in formal semantics of programming languages is required.
Knowledge in the following fields would be welcome:
- The C programming language
- proof environment (e.g. the Coq proof assistant)
- formal specification languages
- program verification

Ville : Palaiseau

Langue / Niveau :

Français : Intermédiaire

Langue / Niveau :

Anglais : Intermédiaire