(Photo credit: Pixabay)
(Photo credit: Pixabay)

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

  • NWO Talent Scheme VIDI 2017
  • File No. 016.Vidi.189.046.
  • February 1, 2019 - January 31, 2024
  • Principal Investigator: Dr. Jorge A. Pérez (University of Groningen, The Netherlands)

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)
  • Joseph Paulus (PhD student, from February 2019)
  • Bas van den Heuvel (PhD student, from October 2019)

Contributors

  • Alen Arslanagić (PhD student)
  • Mauricio Cano (PhD student)

External Collaborators

Work Plan

Sub-project 1:

Reference Framework


(Photo credit: Pixabay)

Sub-project 2:

Static Correctnesss


(Photo credit: Pixabay)

Sub-project 3:

Dynamic Correctness


(Photo credit: Pixabay)

Sub-project 4:

Practical Validation


(Photo credit: Pixabay)

Related Papers

  • 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)
  • The Challenge of Typed Expressiveness in Concurrency (Jorge A. Pérez)

News and Events

  • October 2019: Bas van den Heuvel joins as a PhD student.
  • June 2019: Jorge A. Perez served as co-chair of FORTE'19
  • February 2019: Joseph Paulus joins as a PhD student.
  • February 2019: The project has officially started!

Visitors

2019

Contact

Would you like to know more about the project?

Would you like to work and/or collaborate with us?

Please contact Jorge A. Pérez with any queries related to the project.

Vacancies

  • February 2019: There are no PhD / postdoc positions open at the moment - but stay tuned.
  • If you have your own source of funding (already acquired): send an email to Pérez (subject: “Supervision for Externally Funded PhD”) together with a detailed CV and a motivation letter.
  • BSc and MSc projects are available - excellent students (from Groningen but also elsewhere) should contact Pérez.