CEA-List is renowned for excellence in the use of formal verification methods for the semi-automated analysis of computer code. These methods are particularly valuable in the context of critical systems, notably in the aeronautics industry, and are used to guarantee software safety with respect to both bugs and potential security risks. CEA-List is working on tools to make these methods accessible to a broader community of developers..
CEA-List has developed in-depth knowledge of the field of formal methods. These techniques are used to ensure that source code, whether written by a human developer or automatically generated from a model, is free from bugs and security vulnerabilities. Formal methods are critical to industries like aeronautics, but only a handful of highly specialized experts currently have the ability to use them. The aim of our INCA program is to make formal methods more accessible by developing integrated, intuitive tools any developer—and not just formal methods experts—can use.
The rise of embedded computing is driving an increase in demand for formal verification in a wide range of industries. The automotive industry, where electric vehicles are rapidly gaining traction, is a prime example. The INCA program is helping to bring formal methods to this and other industries.
With this in mind, CEA-List has developed Frama-C, an open-source software suite for developers. Frama-C is designed to be easy to use, with highly automated tools that remove the complexity of formal methods approaches so that non-specialist developers can benefit from them.
In addition to developing ready-to-use, operational code analysis tools for companies, INCA program researchers are continuing to pursue theoretical research on the subject of formal methods.
Our researchers maintain and update analysis models to ensure that they remain compatible with evolving coding languages and new programming paradigms. These analysis also encompass material features, via formal models of targeted systems architectures.
They also work on creating new theoretical frameworks to respond to the latest developments in computing and communication models.
Alongside our work to democratize the use of formal methods across the software development community, the INCA team is also incorporating these approaches into continuous integration pipelines and DevOps. The idea is to automate and systematize source code quality testing to produce safer, better-performing software.
This type of approach will allow companies to release products that are secure by design. Additionally, it offers a solution to the increasingly critical cybersecurity risks associated with the use of IoT devices.
The INCA formal methods team contributes to the ANR SOPRANO project, the European STANCE project, and DARPA’s CHEKOFV project.
