The DaVinci Spring School on formal methods for reactive and quantum systems is an event organised in the context of the DaVinci project, to mark its conclusion. The project focused on building paradigms, foundations, and software engineering method and techniques, to reason about distributed reactive systems in the large, with strong fundamentals grounded on real-time, dynamic logics, relational algebra and quantum computing, among others. As such, the school proposes a set of courses that cover recent advances in these areas, as described below.

This is open to everyone, but for logistic reasons we require everyone to register. Please register here if you plan to attend. Registration will be open until March 23.
Student Presentations
There will be a slot for PhD students who are interested in presenting their ongoing work. Visit here to know more about it.
Local organizer
Guillermina Cledou
Enquiries: mgc (at) inesctec (dot) pt


Day 1: 24 March



Day 2: 25 March




Formal Models and Specifications for Systems of Interacting Components

Modern software systems rely on intensive collaboration, often realised by communication, between computing entities. An important tool for the development of such systems are interface specifications which are needed for the compatible composition and for the correct refinement of components. Both dimensions should work properly together, i.e. compatibility should be preserved by refinement and refinement should be compositional. In this lecture we first analyse solutions and challenges derived from interface theories based on state transition models with I/O-actions (e.g. interface automata, modal I/O-transition systems). Then we look to networks of reactive components and study their communication-safety, i.e. no message loss and no indefinite waiting for response. For this we use the formalism of team automata which supports a broad range of different synchronisation types: (blocking and non-blocking) peer2peer, (strong and weak) broadcast, gathering, etc. Finally, we discuss a variant of dynamic logic suitable to specify properties of the dynamic behaviour of systems of reactive components.
lecture 1, lecture 2
Rolf Hennicker's Short Bio
Rolf Hennicker is an apl. Professor and Academic Director at the Department of Computer Science, University of Munich. His research areas are formal methods in program development with a strong emphasis on reactive components, algebraic specifications, object-oriented software engineering, and environmental systems engineering. His work on observational specifications has been strongly influenced by a cooperation with the ENS de Cachan (France) which originated from a Procope initiative in the early 90ies. Rolf Hennicker has published around 90 peer-reviewed articles in books, journals and conference proceedings. He is and was member of the program committees of many international workshops and conferences (FACS, AMAST, CALCO, SBMF, ..) and he has participated in several national and European projects. Since 2001, Rolf Hennicker is member of the IFIP Working Group 1.3 "Foundations of System Specification". Since 2009 he is member of the steering committees of the International Conferences on Algebra and Coalgebra in Computer Science (CALCO) and of the Workshops on Algebraic Development Techniques (WADT).

Quantum Walks and Search Algorithms

Quantum walks has emerged as one of the main techniques with which we can construct powerful quantum algorithms. This minicourse aims to introduce the most important models of quantum walks and spatial searching algorithms based on quantum walks, alongside a gentle introduction to elements of quantum computing. Afterwards, we will discuss how to implement two models of quantum walks using a superconducting quantum computer, as well as spatial searching.
Bruno Chagas' Short Bio
Bruno Chagas joined ICHEC in January 2020, and he is currently involved in projects in quantum chemistry and Noisy Intermediate-Scale Quantum (NISQ) computers. He obtained his Ph. D. in Computational Modelling at National Laboratory for Scientific Computing (Brazil, 2018), defending his thesis about quantum algorithms based on quantum walks and analysis of its transport properties. Prior to joining ICHEC, Bruno Chagas was a postdoc researcher at Federal University of Minas Gerais, Brazil, researching in physical realizations of Quantum Walks in NISQ computers, and received the certificate of Qiskit Advocate from IBM. Bruno has been working on projects involving quantum walks and optimization algorithms with students in Brazil and Portugal.

(Recent Advances in) Choreography-based Programming

Construction and analysis of distributed systems that consist of message passing processes is hard. Typical challenges include proving deadlock freedom (i.e., the processes never get stuck), proving protocol compliance (i.e., the processes communicate as intended), and proving functional correctness (i.e., the processes compute the intended outcome). Choreography-based programming is a new programming paradigm to overcome these challenges. The idea is to use a new kind of programming artefact---choreographies---to specify and/or implement distributed systems.

In two presentations, I will present the two main approaches to choreography-based programming.

[1] Ruben Hamers, Sung-Shik Jongmans. Discourje: Runtime Verification of Communication Protocols in Clojure. TACAS 2020, LNCS 12078, 266-284. Preprint
[2] Erik Horlings, Sung-Shik Jongmans. Analysis of Specifications of Multiparty Sessions with dcj-lint. ESEC/FSE 2021, 1590-1594. Preprint
[3] Sung-Shik Jongmans and Petra van den Bos. A Predicate Transformer for Choreographies. ESOP 2022, in press. Preprint
lecture 1, lecture 2
Sung-Shik Jongmans' Short Bio
Sung-Shik is an assistant professor in the Department of Computer Science at Open University of the Netherlands. His work focuses on multi-party session types. He is also a visiting researcher in the following institutes: Centrum Wiskunde & Informatica, the Netherlands Foundation of Scientific Research Institutes; Department of Computing, Imperial College London; and Institute for Computing and Information Sciences, Radboud University Nijmegen.

Student Presentations

There will be a slot for PhD students who are interested in presenting their work. This is a valuable opportunity to share ongoing work and get feedback from the various speakers and attendees.
Students will have 15 minutes to present, follow by 5 minutes of QA.
If you are interested in presenting your work, please send an email to mgc (at) inesctec (dot) pt with the following information: