Dr. G. Caltais | People Pages: Find employees & contact details

I am an assistant professor in the Formal Methods and Tools group at University of Twente. Previously, I worked as an independent junior scientist at University of Konstanz, Chair for Software and Systems Engineering, and as a post-doctoral researcher at ETH Zürich, Chair of Software Engineering. I graduated my PhD from Reykjavík University and Radboud University.

My research centers around the formal modelling, specification and analysis of computer systems, with emphasis on automata, formal languages and systems semantics. Areas of interest include:

concurrency theory, causal models, knowledge models, software defined networks, systems and software engineering.

Current projects:

Cyclic Structures in Programs and Proofs: New Harmonies in Software Correctness by Construction [web]
DyNetKAT: a formal framework for dynamic software defined networks [paper] [slides]
Zorro: formal knowldege models for zero downtime [web]

My CV can be found here.

UT students interested in collaborating with me, can review the available (thesis) proposals: [1], [2], [3].

____________________________________

NEWS!

Our OC-XL project was accepted!

____________________________________

Activities & Events (selection):

FSEN'25 SEng@ICT.Open'25 ETAPS blog

____________________________________

(Recent) Committees:

PC: CALCO 2023, ESOP 2023, FORTE 2022/2023, FSEN 2023, IEEE NFV-SDN 2020/2021, SPIN 2022/2024, NFM 2023.

OC: FSEN 2025, STAF 2024, CREST@ETAPS 2019/2023, EXPRESS/SOS 2023, IEEE NFV-SDN 2020-2022, SAC-SVT 2023/2024, SPIN 2023.

Organisations

Affiliated study programs

Courses academic year 2024/2025

Courses in the current academic year are added at the moment they are finalised in the Osiris system. Therefore it is possible that the list is not yet complete for the whole academic year.

Courses academic year 2023/2024

Current projects

Cyclic Structures in Programs and Proofs: New Harmonies in Software Correctness by Construction

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. 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.

This project 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).

Engineering for Zero Downtime in Cyber-Physical Systems via Intelligent Diagnostics

ZORRO

Intelligent Diagnostics, supported by sensor technology and data analytics, can replace traditional human-based diagnosis with AI algorithms to precisely detect anomalies and link them to potential root causes, thus enabling the implementation of appropriate corrective and preventive actions. ZORRO project is centered around addressing significant challenges: Developing reliable and resource-efficient monitoring systems, Incorporating formalised knowledge into the diagnostic workflow, Creating accurate system-level diagnostic algorithms, and Ensuring tight integration within the system's engineering life cycle. Led by Prof. Dr. Mariëlle Stoelinga, ZORRO is a collaborative initiative involving renowned experts from the University of Twente, Saxion University of Applied Sciences, VU Amsterdam, and TNO-ESI.

Finished projects

Causal Reasoning in NetKAT

CReNKAT

We live in a networkcentric world where communication supported by robust an reliable network systems is of real importance. Malfunctioning of network systems can lead to costly losses and even endanger lives. For an example, a widely publicised failure was the crash of the Google server for 40 minutes which, in turn, caused Gmail and Chrome to crash all around the world, leaving millions of users without access to their data. Troubleshooting the issue and identifying the root cause of the event revealed a faulty load balancing configuration which was eventually fixed. This project aims at addressing similar problems, and developing rigorous methodologies for modelling and analysing causes of anomalous behaviours in software defined networks (SDNs). Several big companies including Google, Microsoft, IBM and Nokia are using SDNs to enhance their network infrastructure and operations.

Address

University of Twente

Zilverling (building no. 11), room 3039
Hallenweg 19
7522 NH Enschede
Netherlands

Navigate to location