Public and private contrats for ACSL

Job description: 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.

Your profile: Doctorat en vérification de programme ou sémantique des langages de programmation