Campus Event Calendar

Event Entry

New for: D1, D2, D3, D4, D5

What and Who

Specification and Analysis of C(++) programs with Frama-C and ACSL.

Virgile Prevosto
CEA, Saclay
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2  
Expert Audience

Date, Time and Location

Tuesday, 27 May 2008
60 Minutes
E1 5
rotunda 6th floor


Frama-C is a framework dedicated to build static analyzers for C
programs and make them cooperate to achieve better results. One
important component of this cooperation is the ANSI/ISO C Specification
Language (ACSL), a JML-like language allowing to formally specify the
behavior of C functions and statements. The analyses can indeed
generate verification conditions as ACSL formulas that will be taken as
input by the other ones (and hopefully discharged at some point). This
talk will first present the existing Frama-C analyses. Then, we will
have a look at the main ACSL constructions. Last, we will show how
these constructions can be used for the specification of existing code,
and how Frama-C could be extended to deal with C++.


Brigitta Hansen
0681 9325200
--email hidden
passcode not visible
logged in users only

Brigitta Hansen, 05/27/2008 09:59 -- Created document.