layout: page title: “Challenges of Software Verification Symposium 2025” date: “June 5, 2025” latest_csv: true —

June 5-6, 2025, Venice, Italy

Following the success of CSV 22, CSV 23, and CSV 24, the Symposium on “Challenges of Software Verification” will take place on Thursday 5th and Friday 6th June 2025 in the Aula Baratto of Ca’ Foscari University of Venice. The 2-day event will be organized in several sessions. The scope of the symposium will cover theoretical results in the field of software verification, their practical applications, novel and innovative tools, and their impact of software verification in software engineering and DevOps practices. The symposium will not have published proceedings, but authors of selected abstracts will be invited to submit a full paper to a special issue of the Springer International Journal on Software Tools for Technology Transfer - STTT. The extended version of the talks presented at CSV 2022 has been published in Springer-Nature, the ones of CSV 23 have been published in a special chapter of STTT, and the articles of CSV 2024 have been published and collected in a special issue of STTT.

Tentative Schedule

5 June

   
9:20 Introduction
9:40-10:30 Session: Machine Learning and Verification (chair: Gianluca Caiazza)
9:40 Eleonora Iotti (in collaboration with: Alessio Russo): An Exploration of Machine Learning Techniques and Datasets for Malware Detection [SLIDES]
10:05 Gabriele Penzotti: Challenges in Machine Learning Based Software Vulnerability Assessment [SLIDES]
10:30-11:00 Coffee break
11:00-13:05 Session: Novel Applications of Static Analysis (chair: Gianluca Caiazza)
11:00 Kevin De Porre (in collaboration with: Jim Bauwens, Christophe Scholliers, Elisa Gonzalez Boix): Bridging Interpretation and Verification: A Hybrid Approach to Verifying Distributed Abstractions [SLIDES]
11:25 Cosimo Laneve (in collaboration with: G. Delzanno, A. Sangnier, G. Zavattaro): Decidability problems for Micro-Stipula [SLIDES]
11:50 Marco De Vincenzi (in collaboration with: Chiara Bodei, Gabriele Costa, Ilaria Matteucci): CARBUROS: A Multi-Factor Authentication Protocol for Vehicle-to-Infrastructure Communications [SLIDES]
12:15 Linda Brodo (in collaboration with: Moreno Falaschi, Roberto Bruni, Roberta Gori, Paolo Milazzo): Static analysis and dynamic slicing of Reaction Systems
12:40 Luca Olivieri (in collaboration with: Aradhita Mukherjee, Nabendu Chaki, Agostino Cortesi): Pitfalls of Blockchain Interoperability [SLIDES]
13:05-14:05 Lunch
14:05-16:10 Session: Foundations of Static Analysis (chair: Vincenzo Arceri)
14:05 Benoît Montagu (in collaboration with: Sébastien Bonduelle, Thomas Jensen): Static Analysis for the Dependency of Program Behaviours on their Evaluation Strategy [SLIDES]
14:30 Nicola Assolini (in collaboration with: Alessandra Di Pierro, Isabella Mastroeni ): A Static Analysis of Entanglement [SLIDES]
14:55 Milla Valnet (in collaboration with: Raphaël Monat, Antoine Miné): Compositional Static Value Analysis For Higher-Order Numerical Programs [SLIDES]
15:20 Louis Rustenholz (in collaboration with: Pedro Lopez-Garcia, Manuel Hermenegildo): Abstractions of Sequences, Functions and Operators [SLIDES]
15:45 Isabella Mastroeni (in collaboration with: Marco Campion, Caterina Urban): Measuring vs Abstracting: On the abstraction relation between distances and abstract domains [SLIDES]
16:10-16:40 Coffee break
16:40-18:20 Session: Applications of Static Analysis (chair: Luca Olivieri)
16:40 Caterina Urban (in collaboration with: Naïm Moussaoui Remil): Termination Resilience Static Analysis [SLIDES]
17:05 Ali Rasim Kocal (in collaboration with: Helmut Seidl, Michael Schwarz): Parallelizing a generic fixpoint engine [SLIDES]
17:30 Florian Sihler (in collaboration with: for Ideas/Comments: Johanna Scheck, Oliver Gerstl, Matthias Tichy): Abstract Interpretation to Support Reproducibility of R [SLIDES]
17:55 Paul Robert (in collaboration with: Mihaela Sighireanu, Matthieu Lemerre): Inferring Specification of Pointer Nullness by Abstract Interpretation [SLIDES]
19:00-22:00 Social Dinner

6 June

   
9:00-10:15 Session: Program Verification (chair: Agostino Cortesi)
9:00 Laura Kovacs (in collaboration with: Ivana Bocevska, Anja Petkovic Komel, Michael Rawson, Sophie Rain): Gamifying Blockchain Reasoning [SLIDES]
9:25 Alexander J. Summers (in collaboration with: Zachary Grannan, Aurel Bíly, Jonáš Fiala, Jasper Geer, Markus de Medeiros, Peter Müller): Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees [SLIDES]
9:50 Alessandro Cimatti (in collaboration with: R. Cavada, A. Griggio, C. Lidström, G. Redondi, G. Scaglione, M. Tessi, D. Trenti): Automated Parameterized Verification of a Railway Protection System with Dafny [SLIDES]
10:15-10:45 Coffee break
10:45-12:25 Session: Artificial Intelligence (chair: Maikel Perez Gort)
10:45 Daragh KIng (in collaboration with: Vasileios Koutavas, Laura Kovacs): LLM-based Generation of Weakest Preconditions [SLIDES]
11:10 Alvise Spanò (in collaboration with: Cosimo Laneve, Dalila Ressi, Sabina Rossi, Michele Bugliesi): Assessing Code Understanding in LLMs [SLIDES]
11:35 Davide Taibi: Enhancing Software Verification in the IoT-Edge-Cloud Continuum through Integrated Static and Dynamic Analysis with Generative AI [SLIDES]
12:00 Antonio Emanuele Cinà: Verification Challenges in Machine Learning Security [SLIDES]
13:00-15:00 Lunch

Organizing committee

Agostino Cortesi (University of Venice), general chair

Pietro Ferrara (University of Venice), program co-chair

Vincenzo Arceri (University of Parma), program co-chair

Gianluca Caiazza (University of Venice), local chair

Maikel Lázaro Pérez Gort (University of Venice), web chair

Giacomo Zanatta (University of Venice), publicity chair

Giacomo Boldini (University of Venice), sponsorship chair

Greta Dolcetti (University of Venice), financial chair

Important dates

All dates are tentative and might change in the future.

  • April 1: deadline for abstract submissions
  • April 15: acceptance notification
  • May 20: symposium registration
  • June 5-6: symposium