DaVinci

API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3

API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact)

Branching pomsets for choreographies

Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems

Featured Team Automata

FM 2021

Hubs for VirtuosoNext: Online verification of real-time coordinators

SCP 2021

Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Physical Systems

WiP@RTSS

Implementing Hybrid Semantics: From Functional to Imperative

ICTAC 2020

Verification of Real-Time Coordination in VirtuosoNext (extended version)

VirtuosoNextTM is a distributed real-time operating system (RTOS) featuring a generic programming model dubbed Interacting Entities. This paper focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and …

DaVinci (07/2018-03/2022) - Coordinator until 2021

__Distributed Architectures - Variability and Interaction for Cyber-Physical Systems__ - is an FCT project to analyse interactions among software components considering aspects such as real time and variability. It produced 9 conference publications, 3 journal articles, 1 master thesis, it was involved in the organisation of 3 workshop, an invited tutorial, and a Spring School, and produced several tools available online in http://arcatools.org.