Validation and verification
The List Institute develops methods and tools for the verification and validation of software-intensive systems. These methods have been used worldwide to successfully address software safety and security challenges previously out of the range of traditional verification techniques.
List research teams design and implement automated analysis in order to make software systems more trustworthy, to exhaustively detect their vulnerabilities, to guarantee conformity to their specifications, and accelerate their certification. We collaborate with large-scale industrial ecosystems especially in the field of energy and nuclear power; aeronautic, space, railway, automotive and maritime transport systems; communication; health, or financial sectors.
Among our academic partners
SRI (California), NASA (Virginia), Fraunhofer institute (Berlin), INRIA, CNRS, Université Paris-Saclay, Ecole Polytechnique, Supélec (France).
- Scientific expertise on formal verification and validation methods and tools
- Strong international recognition and collaboration with bodies of reference – Fraunhofer institutes, SRI International, NASA, College University of New York
- Historical and close relations with industrial companies from avionic, railway and nuclear sectors on the most advanced critical systems
- Collaboration with several national and international certification bodies: ANSSI, IRSN, ETSI, NIST
Simulation and virtual platforms for validation
UNISIM is a development environment for virtual platforms that facilitates complex hardware/software simulation and exploration. UNISIM provides a combination of services – debuggers, loaders – allowing the execution and precise observation of the behaviours of a system. It can be used as basis for the development of SystemC simulation modules, for hybrid simulation associating virtual and material components, for non-intrusive software testing and in particular to accelerate hardware-software integration processes.
Automotive, aerospace, energy sectors
- D. August, J. Chang, S. Girbal, D. Gracia-Perez, G. Mouchard, D. Penry, O. Temam, N. Vachharajani. UNISIM: An Open Simulation Environment and Library for Complex Architecture Design and Collaborative Development. Computer Architecture Letters , vol.6, no.2, pp.45-48, Feb. 2007.
- T. Muhammad Khan, D. Gracia-Perez, O. Temam. Combining On-Line Sampling and Adaptive Warm-Up for a More Practical Sampling Strategy. 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools, January 2011.
Source code analysis
Frama-C is a source code analysis platform that leverages approaches such as abstract interpretation, deductive verification, and constraint solving whose common characteristic is to rely on formal methods that ensure their results are rigorously correct. Rooted in an open-source community, this platform is not only a testing ground for various approaches at the service of a variety of users but also a tool that allows combining these different approaches to reach ambitious validation objectives. These analyses are particularly suited to software for which operating safety, or security in the face of malicious behaviours, is crucial.
Nuclear, avionics, railway, maritime, communication, health, finance sectors
- ANR SOPRANO project
- FP7 STANCE project
- DARPA Chekofv (USA) project
- P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, B. Yakobowski. Frama-C - A Software Analysis Perspective. SEFM 2012, LNCS, vol. 7504, pages 233-247. Springer.
- O. Chebaro, P. Cuoq, N. Kosmatov, B. Marre, A. Pacalet, N. Williams, B. Yakobowski. Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1): 107-143 (2014).
Verification and validation of models for critical reactive systems
GATeL is verification and validation suite for SCADE models. These models are used to describe reactive control/command systems especially in the fields of aeronautics, railway and nuclear power. GATeL offers the opportunity to prove properties on these same SCADE models, enabling also model simulation/animation functionalities, test selection criteria definition, automated test generation according to these criteria and their coverage measurement.
Nuclear, railway, avionics sectors
- Cluster Connexion project
- B. Blanc, C. Junke, B. Marre, P. Le Gall, O. Andrieu. Handling State-Machines Specifications with GATeL. MBT 10, ENTCS 264:3, Springer-Verlag, 2010.
- Bruno Marre and Claude Michel. 2010. Improving the floating point addition and subtraction constraints. CP'10, Springer-Verlag, Berlin, Heidelberg, 360-367.
"Designing internationally recognised tools that guarantee software safety and security"
Head of the Software Security Laboratory
+33 1 69 08 00 10