Keynotes

Luís Soares Barbosa, INESC TEC and University of Minho, PT

Paraconsistency for the working software engineer

Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. This lecture summarises recent joint work with Juliana Cunha, Alexandre Madeira and Ana Cruz on a variant of transition systems endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values. Such structures are called paraconsistent transition systems, the qualifier stressing a connection to paraconsistent logic, a logic taking inconsistent information as potentially informative. A coalgebraic perspective on this family of structures is also discussed.

Paula Herber, Universitat Munster, DE

Formal Verification of Cyber-physical Systems using Domain-specific Abstractions

Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring the safety and reliability of cyber-physical systems. Formal methods have the potential to guarantee crucial safety properties under all circumstances, but are incredibly expensive and severely suffer from scalability issues. In this talk, I will summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions.

John van de Wetering, University of Amsterdam, the Netherlands

Picturing Quantum Software

Quantum software is the code that runs on a quantum computer. I’ll give a brief overview of what this means, as well as a trifecta of important challenges in this area: efficient compilation, verification, and classical simulation of quantum programs. Then, I’ll discuss some of the ways we’ve been attacking these problems in recent years, using a number of techniques based on graph rewriting and the ZX calculus.