Representation predicates for deductive verification

Frama-C is a collaborative platform for analysis of C programs. Among the different tools available in Frama-C, WP is dedicated to deductive verification of programs, allowing mathematical proof of functional properties and absence of runtime errors. This tool is used for years in industry.
Separation logic is the most promising way to allow verification of properties for programs involving complex data structures. However, it is hard to use for industrial use-cases. The main reason for this is that it is hard to encode into automatic proof tools. Thus, its use requires a lot of work from users.
The WP tool of Frama-C does not use separation logic. An ongoing research project aims at integrating elements from separation logic into WP, in order to improve performances and the ability to deal with complex data-structures. However, the proposed extension does not allow verifying programs with recursive data-structures, for this, we need the representation precidates from separation logic. The goal of this postdoc is to study how to integrate them in WP.

Post-doctoral position in AI safety and assurance at CEA LIST

The position is related to safety assessment and assurance of AI (Artificial Intelligence)-based systems that used machine-learning components during operation time for performing autonomy functions. Currently, for non-AI system, the safety is assessed prior to the system deployment and the safety assessment results are compiled into a safety case that remains valid through system life. For novel systems integrating AI components, particularly the self-learners systems, such engineering and assurance approach are not applicable as the system can exhibit new behavior in front of unknown situations during operation.

The goal of the postdoc will be to define an engineering approach to perform accurate safety assessment of AI systems. A second objective is to define assurance case artefacts (claims, evidences, etc.) to obtain & preserve justified confidence in the safety of the system through its lifetime, particularly for AI system with operational learning. The approach will be implemented in an open-source framework that it will be evaluated on industry-relevant applications.

The position holder will join a research and development team in a highly stimulating environment with unique opportunities to develop a strong technical and research portfolio. He will be required to collaborate with LSEA academic & industry partners, to contribute and manage national & EU projects, to prepare and submit scientific material for publication, to provide guidance to PhD students.

Application of a MDE approach to AI-based planning for robotic and autonomous systems

The complexity of robotics and autonomous systems (RAS) can only be managed with well-designed software architectures and integrated tool chains that support the entire development process. Model-driven engineering (MDE) is an approach that allows RAS developers to shift their focus from implementation to the domain knowledge space and to promote efficiency, flexibility and separation of concerns for different development stakeholders. One key goal of MDE approaches is to be integrated with available development infrastructures from the RAS community, such as ROS middleware, ROSPlan for task planning, BehaviorTree.CPP for execution and monitoring of robotics tasks and Gazebo for simulation.
The goal of this post-doc is to investigate and develop modular, compositional and predictable software architectures and interoperable design tools based on models, rather than code-centric approaches. The work must be performed in the context of European projects such as RobMoSys (, and other initiatives on AI-based task planning and task execution for robotics and autonomous systems. The main industrial goal is to simplify the effort of RAS engineers and thus allowing the development of more advanced, more complex autonomous systems at an affordable cost. In order to do so, the postdoctoral fellow will contribute to set-up and consolidate a vibrant ecosystem, tool-chain and community that will provide and integrate model-based design, planning and simulation, safety assessment and formal validation and verification capabilities.

Application of ontology and knowledge engineering to complex system engineering

Model-Based System Engineering relies on using various formal descriptions of the system to make prediction, analysis, automation, simulation... However, these descriptions are mostly distributed across heterogeneous silos. The analysis and exploitation of the information are confined to their silos and thereby miss the big picture. The crosscutting insights remain hidden.
To overcome this problem, ontologies and knowledge engineering techniques provide desirable solutions that have been acknowledged by academic works. These techniques and paradigm notably help in giving access to a complete digital twin of the system thanks to their federation capabilities, in making sense to the information by embedding it with existing formal knowledge and in exploring and uncovering inconsistencies thanks to reasoning capabilities.
The objective of this work will be to propose an approach that gives access to a complete digital twin federated with knowledge engineering technologies. The opportunities and limits of the approach will be evaluated on industrial use cases.

Model evolution management and mastering

Designing ever more complex systems needs for new paradigms in order to face all the new challenges as improving safety while reducing time and cost to market. Paradigms, mainly active models and model transformations, promoted by model-driven engineering are providing efficient solutions to deal with those issues. However, as promoted in the series of international workshops on model and evolution (, model (co-)evolution and consistency management become crucial activities to cope with the natural changes of any system. In fact, there is an increasing need for more disciplined techniques and engineering tools to support a wide range of model evolution activities, including model-driven system evolution, model differencing, model comparison, model refactoring, model inconsistency management, model versioning and merging, and (co-)evolution of models.
As part of this project, the LISE want especially to consider model evolution management under both next perspectives:
- The first issue is to enable modelers to manage the evolution of their models. They should be able to follow the changes that have been made within a model by providing as for example “track changes” mode in the modeling environment.
- The second issue concerns the problem of model versioning. The users need here to manage and use multiple versions of their models in a collaborative way.

Integration Testing with Symbolic Execution for Component-Based Systems

Abstract interpretation of ACSL annotations

Frama-C is a set of tools dedicated
to the analysis of C software. In Frama-C, different analyses
techniques are implemented as plug-ins within the same framework.
Part of the glue that holds the various plug-ins together is
the ACSL annotation language. ACSL is a formal specification
language for C programs.
Each verification plug-in is supposed to interpret ACSL
annotations as best it can. A plug-in can also, when it needs to
make an assumption, express it as an ACSL property so that
another plug-in can be used to verify this assumption.

This post-doctoral position consists in improving the precision of Frama-C’s value analysis, based on Abstract Interpretation, for constructs that are not currently handled. The treatment of some constructs will require specific abstract domains to be designed.