Language and software engineering

The research agenda of D4 is to provide the scientific foundations and the accompanying technology for constructing safe, secure and efficient software and systems. The recent convergence between embedded software and cyber-physical systems also induces new challenges in terms of self-management and security, in addition to the traditional issues in efficiency and functional correctness.

This results in two main line of work

• model-based system/software engineering;
• verification and machine-checked program analysis.

Main contributions

• Logical approaches to the verification of cyberphysical systems: open-source, versatile, scheduler synthesizer called ADFG (affine data-flow graphs) using ILPs; proof-/type-based program verification with analysis and inference methods based on abstract interpretation in order to propose modular static analysis methods that use rich types to expose properties of analyzed program modules;
• Software engineering and system of systems modeling: advanced type system for manipulating models in a polymorphic way through different DSL;  interfaces meta-model a new language implementation pattern that enables independent extensibility of the syntax and semantics of metamodel-based software languages; using machine-learning techniques to better understand the existing variability of a software product line; design of an architecture description language for systems of systems;
• Verifying and proving software safety: semantic format for writing operational semantics; static analysis to prove critical C code constant-time execution and protect against side-channel attacks; improving static analysis and extending to hybrid approaches combining static analysis with runtime monitoring; verifying safety properties of system of systems architectures;
• System modeling: theoretical contributions on diagnosability and approximate diagnosability; synthesis algorithms for enforcement monitors from timed automata; contributions to Game theoretic system control and synthesis; modeling of data-centric systems with Petri nets; seminal results on the structural analysis of multimode differential algebraic equations systems.