Program

The workshop will take place on November 28th and 29th.

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

Note for speakers:

  • Contributed talks will be given a slot of ~15 minutes with ~5 minutes for questions.

We are looking forward to meeting you all in Bolzano!

Thursday 28th

Room: C4.01

14:00 — 14:20
Registration
14:20 — 14:30
Welcome and opening of the workshop
Model Checking and Hybrid Systems
Chair: Angelo Montanari
14:30 — 14:50
Model Checking of Optimal LTL and ASAP Properties
Davide Bresolin , Filippo Fantinato , Stefano Tonetta
14:50 — 15:10
On Optimizing Simulation-Based Verification of Cyber-Physical Systems via Statistical Model Checking: a Preliminary Work
Leonardo Picchiami
15:10 — 15:30
Recent results on computable and compositional semantics for hybrid systems
Davide Bresolin , Pieter Collins , Luca Geretti , Roberto Segala , Tiziano Villa
  Coffee break
Formal Methods
Chair: Tiziano Villa
16:00 — 16:20
Temporal Many-valued Conditional Logics: an Abridged Report
Mario Alviano , Laura Giordano , Daniele Theseider Dupre
16:20 — 16:40
Growing HOLMS, a HOL Light Library for Modal Systems
Antonella Bilotta , Marco Maggesi , Cosimo Perini Brogi , Leonardo Quartini
16:40 — 17:00
Towards ASP-based Minimal Unsatisfiable Cores Enumeration for LTLf
Antonio Ielo , Giuseppe Mazzotta , Rafael Peñaloza , Francesco Ricca
17:00 — 17:20
Formalizing decisional and operational roles in legal contracts via term-modal logic
Stef Frijters , Matteo Pascucci
Social Dinner
19:30
Social Dinner
Fink Gasthaus
Via della Mostra 9 — Mustergasse 9

Friday 29th

Room: F0.03

8:30 — 9:00
Registration
Invited talk
Chair: TBA
9:00 — 10:00
Invited talk
Mixing automated temporal planning and ML: the role of opaque entities and RL-based guidance synthesis
Andrea Micheli
 Slides
  Coffee break
Formal Methods for AI - Part 1
Chair: Stefano Tonetta
10:30 — 10:50
Integrating L0 regularization into Multi-layer Logical Perceptron for Interpretable Classification
Gonzalo Jaimovitch-López , Luca Bergamin , Fabio Aiolli , Roberto Confalonieri
10:50 — 11:10
Automated Synthesis of Certified Neural Networks: Initial Results and Open Research Lines
Matteo Zavatteri , Davide Bresolin , Nicolò Navarin
11:10 — 11:30
Towards Modern Rule-Based Learning
Giovanni Pagliarini , Edoardo Ponsanesi , Guido Sciavicco , Ionel Eduard Stan
11:30 — 11:50
Formal Logical Reasoning With Transformers and Their Place on the Chomsky Hierarchy
Stefan Reifberger
  Lunch break
Formal Methods for AI - Part 2
Chair: Davide Bresolin
13:30 — 13:50
Many-Expert Decision Trees
Guillermo Badia , Carles Noguera , Alberto Paparella , Guido Sciavicco
13:50 — 14:10
Evaluating LLMs Capabilities at Natural Language to Logic Translation: A Preliminary Investigation
Andrea Brunello , Riccardo Ferrarese , Luca Geatti , Enrico Marzano , Angelo Montanari , Nicola Saccomanno
14:10 — 14:30
Minimal Rules from Decision Forests: a Systematic Approach
Giovanni Pagliarini , Andrea Paradiso , Marco Perrotta , Guido Sciavicco
Applications
Chair: Leonardo Picchiami
14:30 — 14:50
A Comparison of Machine Learning Techniques for Ethereum Smart Contract Vulnerability Detection
Matteo Rizzo , Dalila Ressi , Andrea Gasparetto , Sabina Rossi
14:50 — 15:10
Run-time monitoring for robot-assisted surgery
Kristina Gogoladze , Natasha Alechina , Zhaoyang Jacopo Hu , Haozheng Xu , Romy van Jaarsveld , Jelle P. Ruurda
  Coffee break
Panel
Chair: Nicola Gigante
15:45 — 16:45
Panel on the relationship between formal methods and AI
Andrea Micheli , Marco Montali , Angelo Montanari
16:45 — 17:00
Closing