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   /   Public and private contrats for ACSL

Public and private contrats for ACSL

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

Abstract

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.

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