> Academic opportunities > PHD positions

Outline Runtime Assertion Checking

Technological challenge: Artificial intelligence & Data intelligence (learn more)

Department: Département Ingénierie Logiciels et Systèmes (LIST)

Laboratory: Laboratoire pour la Sûreté du Logiciel

Start Date:

Location: Saclay

CEA Code: SL-DRT-22-0132

Contact: Julien.Signoles@cea.fr

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. 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. For doing so, E-ACSL performs an heavy implementation of the original source code to insert its own code that monitors the ACSL annotations. This technique is usually refered to as (online) inline runtime verification. However, depending on the context of application, this heavy instrumentation may lead to prohibitive memory and runtime overheads, as well as security concerns. The goal of the PhD consists in designing and implementing an outline runtime verification technique for E-ACSL , compatible with the existing inline technique. Outline runtime verification consists in placing the monitor in an external entity (e.g., another thread, or a remote server) for limiting the instrumentation to communication activities with the remote monitor. While this technique is well known and often applied to monitoring of temporal properties, it was never applied to runtime assertion checking, which raises several challenges regarding the data that need to be monitored.

See all positions Download the offer (.zip)

Email Bookmark and Share