Formal methods are mathematical models and tools to reason about computer systems. Based on the deeply studied theories of automata and logics, they have been successfully applied, for instance, to the automatic verification of control systems, i.e. computer systems whose primary goal is to control other devices (either mechanical, hardware or software). However the mathematical abstractions used to model and verify control systems are not well-suited to systems where data-processing is central (databases, list processing programs).

To model such systems, it is crucial to provide mathematical tools that capture transformational properties between input and output data of programs, rather than just properties of their control flow. While formal methods were focused for a long time on modelling sets of computer behaviours, the challenging scientific issue of building a rich mathematical theory of transformations, which could be applied for instance to complex data-centric systems, has been much less studied.

The objective of this project is therefore to advance the foundations of data transformations and study their application to the verification and automatic synthesis of data-centric systems.

Spokesperson

Emmanuel Filiot

Informatics Department
Faculty of Sciences

Dates
Created on August 31, 2018