Modern life depends on large software systems based on communication.
Different programming techniques already help developers to produce error-free communicating software; unfortunately we know little about how these techniques relate to and complement each other.
This VIDI project will discover the fundamental connections between these techniques and validate them in practice.
PROJECT INFORMATION
File No. 016.Vidi.189.046 [link]
February 1, 2019 - January 31, 2024
Principal Investigator: Dr. Jorge A. Pérez (University of Groningen)
SUMMARY
In computer science, the correctness problem consists in checking that computer systems behave as intended. This long-standing challenge is fundamental today, as most aspects of society depend on communication-based software systems. These systems rely on message-passing programs, which implement complex protocols often exploiting concurrency. A major current challenge is to make these programs respect their intended protocols when deployed in larger systems.
To meet this challenge, this project aims to develop the first unified theory of correctness for message-passing concurrency. We will focus on so-called behavioral type systems that enforce correct message-passing programs by codifying intended protocols as types. These type systems stand out due to their mathematical foundations and independence from specific programming paradigms. Many behavioral type systems exist, but their precision varies ostensibly. As a result, there are as many notions of correctness as there are behavioral type systems; this makes associated verification toolchains hardly interoperable. To overcome this bottleneck, the unified theory will relate the notions of correctness that existing behavioral type systems enforce.
To achieve this aim, various verification techniques for message-passing programs based on behavioral type systems will be rigorously related by applying a new reference framework that will be developed. A key innovation will be the use of the Curry-Howard correspondence for concurrency, the most principled link between computation and logic, to articulate a unified theory of correctness. These developments will crucially exploit our recent underpinning results and our long track record on comparative expressiveness for concurrency. These foundational results will be validated through case studies and tool prototypes.
This project will deliver a sorely missing foundational reference for many advanced verification techniques that target the correctness problem in message-passing concurrency. In the longer term, the project outcomes will ensure that message-passing programs work seamlessly when deployed in society.
TEAM
Funded by the project
Jorge A. Pérez (PI)
Dan Frumin: Postdoc (October 2020 - February 2023)
Joseph Paulus: PhD student (February 2019 - July 2023)
Bas van den Heuvel: PhD student (October 2019 - September 2023) [Thesis]
Contributors
Alen Arslanagić: PhD student [Thesis]
Mauricio Cano: PhD student [Thesis]
External Collaborators
Luís Caires (NOVA University Lisbon, Portugal)
Daniele Nantes (University of Brasilia, Brazil)
Nobuko Yoshida (Imperial College London, UK)
NEWS, EVENTS AND VISITORS
2024
January 31st: The project officially ends.
2023
Jorge A. Pérez
has served as PC member of ESOP 2023, PLDI 2023, EXPRESS/SOS 2023, FM-BPM 2023, ST 30.
2022
Jorge A. Pérez
has served as PC member of PLACES 2022.
2021
Jorge A. Pérez
has served as PC member of FORTE'21, LSFA'21, TYPES 2021, PPDP'21, FACS 2021.
was an invited speaker at the OWLS (Online Worldwide Seminar on Logic and Semantics). The slides are here.
2020
Kirstin Peters (TU Darmstadt) visited our group on February 24-27.
Claudio Mezzina (University of Urbino, Italy) visited our group on January 20-21.
Jorge A. Pérez served as
Co-organizer of the SEN Symposium 2020: the Sixth Dutch national symposium on Software Engineering
PC member of PLACES'20, CONCUR'20, EXPRESS/SOS'20.
2019
Jorge A. Pérez served as co-chair of FORTE'19
Peter Mosses (Swansea University & TU Delft) visited our group on November 13. Bernoulli Colloquium: "CBS: Component-based specification of programming languages".
Yehia Abd Alrahman (Gothenburg University, Sweden) visited our group on October 2-4. Bernoulli Colloquium: "A Computational Framework for Adaptive Systems and its Verification".
Meeting with the project's user committee on November 15.
Bas van den Heuvel joins as a PhD student on October 1st.
Silvia Ghilezan (Novi Sad, Serbia) visited our group from May 20-24. Bernoulli Colloquium: "Types in logic, computation and concurrency - an overview".
Emanuele D'Osualdo (Imperial College, UK) visited our group on May 17 (a short visit, after this Lorentz Center workshop).
Nobuko Yoshida (Imperial College, UK) visited our group from March 26-29. Bernoulli Colloquium: "Behavioural Type-Based Static Verification Framework for Go".
Jurriaan Rot (UCL and Radboud University) visited our group on March 20. Bernoulli Colloquium: "Coalgebra Learning via Duality".
Daniele Nantes (Brasilia, Brazil) visited our group from January 21 - February 14.
Joseph Paulus joins as a PhD student on February 1st.
February 2019: The project has officially started!
WORK PLAN
PAPERS
(See also here)
2019
Domain-Aware Session Types (Luis Caires, Jorge A. Pérez, Bernardo Toninho, and Frank Pfenning)
Minimal Session Types (Alen Arslanagic, Jorge A. Pérez, and Erik Voogd)
ECOOP'19 LIPIcs, Vol. 134. [DOI] [DRAFT@arxiv (with appendices)] [artifact]
Earlier
CONTACT
Would you like to know more about the project?
Would you like to work and/or collaborate with us?
Please contact us with any queries related to the project.