Phd and internship subjects
PhD subjects
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 goal of this PhD project is to devise a decision procedure for Separation Logic with user-provided inductive definitions of predicates. We intend to find 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 data theory reasoning based on external tools (to take into account the properties of the data stored inside the structure).
Internship subjects
The goal of this internship is the study of logics for the design and verification of complex component-based distributed applications, using the principles of locality (the ability to describe the effect of an update only from the parts involved while gnoring the ones unchanged) and compositionality (the ability to join the results of local analyses into a global condition capturing the correctness requirement for the entire system). During this internship, the candidate will aquire command of advanced theoretical notions of logics and system verification. The internship comprises theoretical as well as implementation work.
The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency.
The goal of this internship is to study the combination of Separation Logic with data theories supported by SMT solvers. The internship comprises theoretical as well as implementation work.
