| Acronym: STT |
| Main Objective: Our goal is the development of static analysis systems to verify safety and liveness properties of concurrent distributed systems specified in calculi of mobile processes. The properties we are interested in are not only behavioural, like deadlock freedom or conformance to a protocol, but also structural (or spatial), like connectivity or resource usage. The existing systems treat only some of the behavioural properties, in a limited way (not purely static, or in very restricted settings). Building on existing work on behavioural types and on spatial logics, we aim at the development of richer notions of types, able of expressing behavioural and spatial properties of distributed systems. We envisage expressive, yet decidable and computationally tractable static analysis systems, which allow to formally prove that a process enjoys a certain property, and that there will be no run-time property violations. |
| Reference: POSC/EIA/55582/2005 |
| Funding: FCT/POSC |
| Start Date: 01-07-2005 |
| End Date: 01-06-2008 |
| Team: António Maria Alarcão Ravara, Maxime Emile Gamboni |
| Groups: Network Architectures and Protocols – Lx |
| Partners: CITI (Centro de Informática e Tecnologias da Informação, FCT/UNL), with Researchers Luis Caires and Vasco Vasconcelos |
| Local Coordinator: António Maria Alarcão Ravara |
| Links:
http://www.math.ist.utl.pt/%7Eamar/projectos/fct/spacetimetypes.html Internal Page |
|
|
|
Associated Publications
|
