CEA is a public multidisciplinary research organization whose research fields range from nuclear industry to biosciences and fundamental physics. It is made of several research centres located in France.
CEA represents: 15024 employees, 2.7 B Euros budget, 1689 patents registered or active, 1300 contracts signed with industry, 83 new companies created since 1984 in high technologies sectors, 9 research centres. (http://www.cea.fr/default_gb.htm)
The CEA-LIST department combines basic research and industrial R&D and is primarily concerned with the development of technologies that combine software and hardware to form highly integrated complex systems. The research activities are structured into three major themes: embedded systems, interactive systems and sensors and signal processing. CEA-LIST focuses on methods and tools for the design of embedded systems with appropriate architectures, software, and an optimal level of safety.
Within CEA-LIST, the LSL (Laboratoire de Sureté Logicielle, Software Safety Lab) is focused on the verification & validation of software and hardware components. The LSL develops methods and tools for the static analysis and test case generation of safety-critical applications.
CEA-LIST has participated to several international and national research projects in the above mentioned fields, within the FP6, RNTL, ANR and ITEA Programmes.
CEA-LIST will undertake the development of evolutions of the Frama-C toolkit in order to handle the analysis of the C++ and Java programming languages. Much research is involved in finding solutions to fundamental language-dependent problems. Next, CEA-LIST will develop security-dedicated plug-ins to analyse the security properties inherent to the applications of the project.
Armand Puccetti, Dr., is a Research Engineer at CEA-LIST where he is working in the Software Safety Laboratory. He is involved in several European research projects, namely in the MEDEA+ programme. His research interests include formal methods for software and hardware description languages, semantics of programming languages, theorem provers, compilers and event-based simulation techniques. Before moving to CEA-LIST in 2000, he was employed as a Project Manager at C-S, a privately owned software house where he participated to diverse software development or applied research projects, ranging from CASE tools and compiler development to military simulation tools and methods. He graduated from INPL (http://www.inpl-nancy.fr) where he earned a PhD in1987.
Virgile Prevosto, Dr., is a Research Engineer at CEA-LIST where he is working in the Software Reliability Laboratory. His research interests include formal methods for software verification tool verification, formal specifications, theorem provers, semantics of programming languages and compiler techniques. Before moving to CEA-LIST in 2006, he worked at the Max-Planck institute for Informatics, Germany (http://www.mpi-inf.mpg.de) where he was involved in the Verisoft project (http://www.verisoft.de) and at INRIA, France (http://www.inria.fr). He earned an engineering degree and a master degree from the Ecole Polytechnique, France (http://www.polytechnique.edu) and in 2003 a PhD from the University of Paris 6 (subject: formalization and implementation of an environment for the specification and verification of software libraries).