The Science Board of NWO has awarded 64 million euros for groundbreaking fundamental research to 21 consortia, in the Open Competition Domain Science-XL 2023-2024. This funding enables researchers to initiate, strengthen, or expand world-class research initiatives collaboratively. On 17 December it was announced that one member of the EEMCS faculty is among the recipients of the grants: Georgiana Caltais.
Georgiana Caltais, from the Formal Methods and Tools group (FMT), is a co-applicant of the project “Cyclic Structures in Programs and Proofs: New Harmonies in Software Correctness by Construction”. The project has been awarded 3 million euros. It is run by an outstanding team: Henning Basold (Leiden University), Georgiana Caltais (University of Twente), Jesper Cockx (TU Delft), Helle Hvid Hansen (University of Groningen), and Robbert Krebbers (Radboud University Nijmegen), under the leadership of Jorge Perez (University of Groningen).
The project aims to improve software reliability by exploring the concept of cyclic structures such as loops in programs, circular communication protocols, and feedback mechanisms in control systems. Cyclic structures come in two forms: some describe processes that eventually stop (inductive structures), while others represent systems designed to run continuously and interact with their environment (coinductive structures). Understanding and verifying these cyclic behaviours is a major challenge in creating reliable software, especially because real-world systems often combine inductive and coinductive structures in complex ways. Current tools and methods are not yet capable of fully analysing such systems, leaving a gap between theoretical models and practical applications. To bridge this gap, they will develop new techniques and tools that unify theory and practice using advanced mathematical principles like coalgebra and coinduction.
The proposed approach covers three facets of the development process for reliable software:
(1) Reliability by Proof - focused on developing foundational methods and tools for cyclic proofs using coalgebraic modal logic to ensure the correctness of systems with cyclic structures;
(2) Reliability by Construction - emphasising the compositional verification of interacting programs based on behavioural type systems and their coalgebraic formulations;
(3) Reliable Proofs by Certification - enhancing proof assistants like Coq and Agda with advanced capabilities for coinductive reasoning, enabling more robust verification of software properties.
This research will push the boundaries of software verification, enhancing areas such as Logic, Programming Languages, Type Theory, Concurrency, and Proof Assistants. Ultimately, it will expand the capabilities of modern tools like Agda and Coq, to verify the behaviour of real-world software written in languages like Rust, paving the way for more reliable and robust systems.
The consortium will support the work of 9 PhD students and postdocs over the next 5 years.
