Accueil > Axes > MOHYTOS > Emplois et stages > Emplois et stages
Emplois et stages
Emplois et stages
Thèse
- PhD position : Encoding and Sampling of Constrained Signal Spaces for Validation of CPS
- PhD position : Proving Correctness of Reconfigurable Systems
The goal of this PhD project is the development of a rigourous design framework for distributed systems, that uses verification from the early stages of model building. Formal verification is the process of transforming a query about the correctness of a system (e.g. is every store request to a cloud treated by storing the data in such a way that any future retrieval request will eventually find it ?) into a logical validity query (is a given formula true in general ?) that can be handled by automated reasoning techniques (theorem proving). Hence, we recognise logic, automated reasoning and model checking as being the main ingredients of formal verification, and also central research topics in our project.
The successful candidate is expected to work on logics for high-level reasoning about parameterized architectures of distributed systems. The decision problems of these logics will be studied from a theoretical point of view, such as existence of proof systems and the complexity of related algorithms. The architecture description logics will be used to verify systems by parameterized model checking techniques based on e.g., invariant synthesis and automata learning. We plan on implementing proof-of-concept prototype tools and performing experiments on models of real-life systems (inter-blockchain communication, mobile applications, etc.)
- PhD Position : Decision Procedures for Inductive Separation Logic Modulo Data Theories
The goal of this PhD project is to devise a procedure that is optimal from a theoretical point of view, practically efficient, and able to handle a class of definitions that is as large as possible, combining spatial reasoning (to reason on the shape of the considered data structures) with theory reasoning based on external tools (to take into account the properties of the data stored inside the structure).
