Projects  •

LIVENESS

Full Title
LIVENESS - Liveness, statically
Description

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.
Funding Entity
FCT
Start Date
20/03/2012
End Date
19/09/2015
Coordinator
NOVA ID FCT
Partners
NOVA ID FCT, FFCUL (LaSIGE)
Team at LASIGE
Status
Closed