About us
Espace utilisateur
Education
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Thesis
Home   /   Post Doctorat   /   Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C programs

Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C programs

Computer science and software Cyber security : hardware and sofware Engineering sciences Technological challenges

Abstract

Our team develops Frama-C (http://frama-c.com), a code analysis platform for C programs which provides several analyzers as plug-ins. Frama-C itself is developed in OCaml. 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
including abstract interpretation, weakest preconditions calculus, and runtime assertion checking. E-ACSL is the Frama-C plug-in dedicated to runtime assertion checking. It converts a C program extended with formal annotations written in a subset of ACSL into a new C program which checks the validity of annotations at runtime: by default, the program execution stops whenever one annotation
is violated, or behaves in the same way than the input program if all its annotations are valid. One key feature of E-ACSL is the expressivity of its specification language which allows the user to describe powerful safety and security properties. Another key feature is the efficiency of the generated code which relies on a custom memory library and dedicated static analyses. However E-ACSL can still be improved in many ways in order to extend its expressivity and to reduce its memory and time overheads. It is the goal of this postdoc position.

Laboratory

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down