NOTE! This site uses cookies and similar technologies.

If you not change browser settings, you agree to it. Learn more

I understand

Learn more about cookies at : http://www.aboutcookies.org/Default.aspx?page=1

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).

Assets

  • 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

Major technologies

Simulation and virtual platforms for validation

Description

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.

Applications

Automotive, aerospace, energy sectors

Major projects

Publications

 

Source code analysis

frama c

Description

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.

Applications

Nuclear, avionics, railway, maritime, communication, health, finance sectors

Major projects

  • ANR SOPRANO project
  • FP7 STANCE project
  • DARPA Chekofv (USA) project

Publications

 

Verification and validation of models for critical reactive systems

gatel montage 3

Description

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.

Applications

Nuclear, railway, avionics sectors

Major projects

Publications