Projects •
LIVENESS
Full Title
LIVENESS - Liveness, staticallyDescription
The main objective of the project is the development of automatic solutions to guarantee liveness properties of distributed, collaborative, communication-centred, software systems and applications.
Specifically, our objectives are the following:
- Pursue a semantical approach to types for concurrency: we want to study the expressiveness of languages like session-, or conversation-, types, looking for decidability and complexity results;
- Develop type systems for various settings, from process calculi to programming languages, able of ensuring liveness properties like the absence of races, deadlocks, or livelocks, and like activeness (ability to establish a connection) and responsiveness (ability to conduct a conversation for each connection), progress and termination;
- Study generic type systems using spatial logics and ensuring general properties, either existential (some run of the system enjoys of a property from some moment on) or universal (all runs of the system enjoys of a property from some moment on);
- Develop prototypes, integrating the type systems with model checkers and with compilers for core programming languages.