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
10:05 Gabriele Penzotti: Challenges in Machine Learning Based Software Vulnerability Assessment
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
11:25 Cosimo Laneve (in collaboration with: G. Delzanno, A. Sangnier, G. Zavattaro): Decidability problems for Micro-Stipula
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
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
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
14:30 Nicola Assolini (in collaboration with: Alessandra Di Pierro, Isabella Mastroeni ): A Static Analysis of Entanglement
14:55 Milla Valnet (in collaboration with: Raphaël Monat, Antoine Miné): Compositional Static Value Analysis For Higher-Order Numerical Programs
15:20 Louis Rustenholz (in collaboration with: Pedro Lopez-Garcia, Manuel Hermenegildo): Abstractions of Sequences, Functions and Operators
15:45 Isabella Mastroeni (in collaboration with: Marco Campion, Caterina Urban): Measuring vs Abstracting: On the abstraction relation between distances and abstract domains
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
17:05 Ali Rasim Kocal (in collaboration with: Helmut Seidl, Michael Schwarz): Parallelizing a generic fixpoint engine
17:30 Florian Sihler (in collaboration with: for Ideas/Comments: Johanna Scheck, Oliver Gerstl, Matthias Tichy): Abstract Interpretation to Support Reproducibility of R
17:55 Paul Robert (in collaboration with: Mihaela Sighireanu, Matthieu Lemerre): Inferring Specification of Pointer Nullness by Abstract Interpretation
19:00-22:00 Social Dinner

6 June

9:00-10:40 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
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
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
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
11:10 Alvise Spanò (in collaboration with: Cosimo Laneve, Dalila Ressi, Sabina Rossi, Michele Bugliesi): Assessing Code Understanding in LLMs
11:35 Davide Taibi: Enhancing Software Verification in the IoT-Edge-Cloud Continuum through Integrated Static and Dynamic Analysis with Generative AI
12:00 Antonio Emanuele Cinà: Verification Challenges in Machine Learning Security
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