The program will be conducted completely online, using the following time slots:

  • Tuesday 18 May 14:00 17:00 CET
  • Wednesday 19 May 14:00 17:00 CET
  • Thursday 20 May 10:00 13:00 CET
  • Friday 21 May 14:00 17:00 CET

For details see

There will be two keynotes:

  1. Moshe Y. Yardi (Rice University, Austin, Houston, USA) will give a keynote titled Program Verification: a 70-Year HistoryAbstract: "The year 2019 saw the 70th anniversary of Alan Turing's paper "Checking a Large Routine", and the 50th anniversary of Tony Hoare's paper, "An Axiomatic Basis for Computer Programming". In that paper, Hoare stated: "When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics. In this talk, I will review the 70+-year history of this vision, describing the obstacles, the controversies, and progress milestones. I will conclude with the description of both impressive progress and dramatic failures exhibited over the past few years."
  2. Liliana Pasquale (University College Dublin & Lero, Ireland) will give a keynote titled Towards Formalising Sustainable Security. Abstract: "Cyber-physical systems, such as smart buildings, cities, and industrial control systems are increasingly managed by software. As the cyber and physical spaces characterizing a software system operating environment are becoming more intertwined, their attack surface has increased and they have become more targeted by attackers. Considering the critical applications of CPS, adversaries can interrupt the functionality of critical infrastructure, also possibly causing human loss. Thus, CPS should be designed to adapt their security controls dynamically, in order to continuously protect valuable assets from harm and satisfy security goals at runtime (during execution). However, research in the adaptive security domain has rarely focused on mitigating unexpected security threats at runtime. Changes of security controls can affect satisfaction of safety-critical properties of a CPS and lead stakeholders (e.g., users and engineers) to lose trust in the system. This can even be more detrimental considering that stakeholders may need to actively monitor data, support decision making and/or execute security controls, in order to avoid security requirements violations.

    The objective of this talk is to propose the notion of sustainable security systems. Such systems will be capable of detecting new/changing threats and identify effective security controls dynamically. Also, they will endure engagement of the stakeholders in their operation and use. This talk will explore existing key research approaches that have been proposed to:
    · Formalise adaptive security (cyber-physical) systems and detect/mitigate unexpected security threats at runtime
    · Support runtime verification of large-scale (cyber-physical) systems
    · Assure and explain adaptive security systems
    The keynote will highlight research gaps and challenges towards formalising sustainable security systems and will outline a research agenda to tackle these challenges."


The following papers and short papers will be part of the program (details will be added soon):

  • Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella and Mieke Massink. Feasibility of Spatial Model Checking for Nevus Segmentation
  • Rania Taleb, Raphael Khoury and Sylvain Hallé. Runtime Verification Under Access Restrictions
  • Marie-Christine Jakobs. PEQcheck: Localized and Context-aware Checking of Functional Equivalence
  • Alexander Knüppel, Leon Schaer and Ina Schaefer. How much Specification is Enough? Mutation Analysis for Software Contracts
  • Tomas Kulik, Jalil Boudjadar and Diego F. Aranha. Formally Verified Credentials Management for Industrial Control Systems
  • Raelijohn Erick, Michalis Famelis and Houari Sahraoui. Checking temporal patterns of API usage without code execution
  • Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling and Pascale Le Gall. Methodology for Specification and Verification of High-Level Properties with MetAcsl
  • Robert L. Smith, Marcello M. Bersani, Matteo Rossi and Pierluigi San Pietro. Improved Bounded Model Checking of Timed Automata
  • Omar Al Bataineh, Arvind Easwaran and Daniel Ng Jun Xian. Monitoring Cumulative Non-functional Properties
  • Lukas Armborst and Marieke Huisman. Permission-Based Verification of Red-Black Trees and Their Merging
  • Besma Khaireddine and Ali Mili. Quantifying Faultiness: What Does It Mean to Have N Faults
  • Lucia Nasti, Roberta Gori and Paolo Milazzo. Formal characterization and efficient verification of a biological robustness property
  • Alexander Knüppel, Thomas Thüm and Ina Schaefer. GUIDO: Automated Guidance for the Configuration of Deductive Program Verifiers