Friday 4th October, 2013
4:00pm to 4:20pm
Whether software is embedded into a critical system or used off-the-shelf by millions of users, it is having to meet an increasingly difficult requirement: the need to guarantee its pivotal properties. Can the software produce unspecified behaviors ? Does it contain a security vulnerability ? Does it isolate its components from one another ? Does it meet its specifications ? Frama-C is an open-source platform for the modular analysis of C source code. Its design allows users and developers to perform complementary verifications, providing guarantees about its behavior through static or dynamic analyses. By means of an open and modular architecture, it enables the development of new plug-ins by a growing community of both academic and industrial users. In this talk we will review some of the main features of the Frama-C platform, show how it can be successfully applied to (open-source) software projects, and illustrate its role in various collaborations and shared innovation contexts.
engineering-researcher, CEA Tech
François Bobot is an engineering-researcher at CEA Tech working on software verification and automatic provers. He received a Phd in Computer Science from Paris-Sud University. During his thesis, he worked on making the specification of program using pointers easier by simplifyng the expression of separation properties. He also help the use of differents automatic and assisted provers throught the development of the Why3 tool.
4:20pm Implementing quality in Java projects by Vincent Massol
Sign in to add slides, notes or videos to this session