Détail de l'offre
Entité de rattachementLe Commissariat à l'énergie atomique et aux énergies alternatives (CEA) est un organisme public de recherche.
Acteur majeur de la recherche, du développement et de l'innovation, le CEA intervient dans le cadre de ses quatre missions :
. la défense et la sécurité
. l'énergie nucléaire (fission et fusion)
. la recherche technologique pour l'industrie
. la recherche fondamentale (sciences de la matière et sciences de la vie).
Avec ses 16000 salariés -techniciens, ingénieurs, chercheurs, et personnel en soutien à la recherche- le CEA participe à de nombreux projets de collaboration aux côtés de ses partenaires académiques et industriels.
Description de l'unité
The Software Safety and Security Laboratory (LSL) at CEA List Institute has an ambitious goal : help designers, developers and validation experts ship high-confidence systems and software. Objects in our surroundings are getting more and more complex, and we have built a reputation for efficiently using formal reasoning to demonstrate their trustworthiness. In collaboration with the most creative people in academia and the industry, we design methods and tools that leverage innovative approaches to ensure that real-world systems can comply with the highest safety and security standards. Our organizational structure is simple : those who pioneer new concepts are the ones who get to
implement them. We are a forty-person team, and your work will have a direct and visible impact on the state of formal verification. CEA LIST's offices are located at the heart of Campus Paris Saclay, in the largest European cluster of public and private research.
Description du poste
Mathématiques, information scientifique, logiciel
Intitulé de l'offre
6-month Master Internship on Formal Semantics of the Specification Language ACSL H/F
Sujet de stage
The internship will be dedicated to provide a formal semantics to ACSL, the ANSI/ISO C Specification language (https://github.com/acsl-language/acsl) that is at the heart of the Frama-C code analysis platform (https://frama-c.com/), in order to ensure that all Frama-C plug-ins share a common understanding of each ACSL annotation. This internship can easily morph into a PhD thesis topic for interested candidate.
Durée du contrat (en mois)
Description de l'offre
Our team developsFrama-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 theACSLspecification 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 thelingua francashared 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 thereference manualwritten 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.CompCertmemory model,the executable semanticsformalized in the K framework, or Robbert Krebber'sPhD thesis), expanding upon the work done by Paolo Herms in hisPhD thesison the implementation of a certified verification condition generator. Ideas could also come from similar works for other specification languages such asJML. 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.
Moyens / Méthodes / Logiciels
the intern will be provided with a workstation under Linux (preferred) or Windows
Profil du candidat
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