The workshop will take place on Wednesday September 22nd, in partial overlap with GandALF 2021.

The program of the workshop includes a rich set of presentations from all the OVERLAY thematic areas, and a great invited talk shared with GandALF 2021.

Note for speakers:

  • Contributed talks will be given a slot of ~13 minutes (we consider a 2 minutes buffer to change the speaker and for possible technical problems). We would like to leave more room for discussion so we suggest to organize your time in order to reserve approximately 8 minutes for the talk and 5 minutes for the discussion.
  • Note that presentations will be recorded and made public, unless speakers express their disagreement by writing an email to the workshop organizers.

We are looking forward to meeting you all in Padua (or virtually)!

Wednesday 22nd

All times are Central European Summer Time (UTC+2)
8:50 — 9:00
Welcome and opening of the workshop
Invited talk
9:00 — 10:00
Invited talk • Shared with GandALF 2021
Shield Synthesis for Safe Reinforcement Learning
Roderick Bloem
  Coffee break
Planning and Temporal Reasoning
10:45 — 11:00
Planning with Global State Constraints for Urban Traffic Control
Franc Ivankovic, Marco Roveri
11:00 — 11:15
BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker
Luca Geatti, Nicola Gigante, Angelo Montanari
11:15 — 11:30
Automated Planning Through Program Verification
Salvatore La Torre, Gennaro Parlato
11:30 — 11:45
Rule-based Shield Synthesis for Partially Observable Monte Carlo Planning
Giulio Mazzi, Alberto Castellini, Alessandro Farinelli
Analysis of complex models
11:45 — 12:00
Dynamic Attack Trees
Aliyu Tanko Ali, Damas Gruska
12:00 — 12:15
Mining Temporal Networks: Results and Open Problems
Guido Sciavicco, Tiziano Villa, Matteo Zavatteri
12:15 — 12:30
Multi-Frame Modal Symbolic Learning
Giovanni Pagliarini, Guido Sciavicco, Ionel Eduard Stan
12:30 — 12:45
Synthesizing model completions from temporal logic specifications with incomplete knowledge
Serenella Cerrito, Valentin Goranko, Sophie Paillocher
  Lunch break
Reasoning and Verification
14:30 — 14:45
Automated Reasoning for Reinforcement Learning Agents in Structured Environments
Alessandro Gianola, Marco Montali, Matteo Papini
14:45 — 15:00
Using Directional Arc Consistency with Asynchronous Forward-Bounding algorithm
Rachid Adrdor, Lahcen Koutti
15:00 — 15:15
Statistical Model Checking for the Analysis of Mission- and Safety-Critical Cyber-Physical Systems
Angela Pappagallo
15:15 — 15:30
On the Parameterized Verification of Abstract Models of Contact Tracing Protocols
Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier
Learning, neural networks, and their applications
15:30 — 15:45
Towards Learning From Graph Representable Formal Models
Marco Sälzer, Georg Siebert
15:45 — 16:00
A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks
Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, Andrea Peruffo
16:00 — 16:15
Ranking Model Checking Backends for Automated Selection via Classification and Regression Learning
Jannik Dunkelau, Leo Baldus
16:15 — 16:30
Preferential Reasoning with Typicality and Neural Network Models (Extended Abstract)
Laura Giordano, Valentina Gliozzi, Daniele Theseider Dupré
  Coffee break
Tools and Applications
17:15 — 17:30
Reverse engineering with P-stable Abstractions
Anna Becchi, Alessandro Cimatti, Enea Zaffanella
17:30 — 17:45
AI-guided optimal deployments of drone-intercepting systems in large critical areas
Marco Esposito
17:45 — 18:00
QUGA - Quality Guarantees for Autoencoders
Benedikt Böing, Rajarshi Roy, Daniel Neider, Emmanuel Müller
18:00 — 18:15
Simulation-Based Synthesis of Personalised Therapies for Colorectal Cancer
Marco Esposito, Leonardo Picchiami
18:15 — 18:30