About
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.
- Where: Anfiteatro A1, Dep. Informática, Universidade do Minho
- When: 24-25 March 2022
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
Courses
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.
Slides
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.
Slides
lecture
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.
-
In the "choreographies-as-types" approach, choreographies are used as specifications of
distributed systems against which implementations can be checked for compliance. I will
explain the choreographies-as-types approach in the context of recent TACAS'20 and
ESEC/FSE'21 papers [1,2]. The main contribution of these papers is a runtime verification
framework (reminiscent of service orchestration) to support the choreographies-as-types
approach in practice.
-
In the "choreographies-as-programs" approach, choreographies are used as implementations
of distributed systems. I will explain the choreographies-as-programs approach in the
context of a recent ESOP'22 paper [3]. The main contribution of this paper is a predicate
transformer for choreographies (reminiscent of Dijkstra's weakest preconditions) to reason
about functional correctness.
[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
Slides
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.
Organization
Students will have 15 minutes to present, follow by 5 minutes of QA.
Registration
If you are interested in presenting your work, please send an email to
mgc (at) inesctec
(dot) pt with the following information:
- Title of the thesis
- A short abstract that summarises the work to be presented
- Name of the supervisor
