Public and private contrats for ACSL

Frama-C is a collaborative platform for the analysis of C programs. It provides a specification language named ACSL, which is based on the notion of contracts. These contracts, provided though code annotations, enable specification of the expected behavior of the different functions of a program. It is then possible to check that the program conforms to the user-provided specification thanks to the different analyzers provided by Frama-C.
An important limitation about the contracts in the current version of ACSL with respect to the C programming language is that they do not allow specifying different contracts (internal/private, external/private) for a module when this module does not export all details of the implementation to the external modules. For this, differentiating public contract and private contract is necessary, but also how to link them together so that the global consistency of specification and analysis is assured.

Application of formal methods for interferences management

Within a multidisciplinary technological research team of experts in SW/HW co-design tools by applying formal methods, you will be involved in a national research project aiming at developing an environment to identify, analyze and reduce the interferences generated by the concurrent execution of applications on a heterogeneous commercial-off-the-shelf (COTS) multi-core hardware platform.