June 6-7, 2024, Venice, Italy

Following the success of CSV 22 and CSV 23, the Symposium on “Challenges of Software Verification” will take place on Thursday 6th and Friday 7th June 2024 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. The extended version of the talks presented at CSV 2022 has been published in Springer-Nature, while the articles submitted at CSV 2023 are currently under review for a special issue of the Springer-Nature International Journal on Software Tools for Technology Transfer.

Tentative Schedule

6 June

9:15-9:30 Welcome
9:30-11:00 Session: Practical aspects of static analysis and tools
Raphaël Monat (joint work with Abdelraouf Ouadjaout and Antoine Miné): “Tools and techniques to ease maintenance of academic static analyzers”
Francesca Scozzari (joint work with Gianluca Amato): “Experimental results on optimal abstract operators for sharing and linearity”
Idriss Riouak (joint work with Görel Hedin, Niklas Fors and Christoph Reichenbach): “IntraJ: A Demand-driven Framework for Intraprocedural Java Code Analysis”
11:00-11:30 Coffee break
11:30-13:00 Session: Analysis and Verification by Abstract Interpretation
Isabella Mastroeni: “Enforcing Abstract Robustness for Classifiers: New ideas”
Michael Schwarz (joint work with Julian Erhard and Helmut Seidl): “Digests for Seamlessly Improving Precision of Abstract Interpretation of Multi-Threaded Programs”
Matteo Boroni Grazioli (joint work with Vincenzo Arceri, Greta Dolcetti and Enea Zaffanella): “Faster Static Analysis with Abstract Compilation”
13:00-14:00 Lunch break
14:00-16:00 Session: Program verification and model checking
Gianluca Redondi (joint work with Alessandro Cimatti, Alberto Griggio): “Checking Invariants of systems with SMT theories and quantifiers”
Peter Müller (joint work with Marco Eilers, Thibault Dardinier): “CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity”
Demis Ballis (joint work Linda Brodo, Moreno Falaschi, Carlos Olarte): “Verification of Reaction Systems in Rewriting Logic”
Dina Borrego (joint work with Elisa Gonzalez Boix (VUB), Carla Ferreira (NOVA)): “Designing and Verifying conflict free mechanism to maintain application invariants in replicated environments”
16:00-16:30 Coffe break
16:30-18:30 Session: Software engineering
Federico Serafini (joint work with Roberto Bagnara, Abramo Bagnara, Nicola Vetrini): “Memory Safety for C-rusted: Challenges and Possible Solutions”
Alessandro Cimatti (joint work with Lorenzo Cappelletti, Roberto Cavada, Marco Keppel, Lorenzo Pilati): “A retrospective application of formal methods to the development of safety-critical software”
Fabiano Pecorelli (joint work with Antonio Trovato, Manuel De Stefano, Dario Di Nucci, and Andrea De Lucia): “Reformulating Regression Test Case Selection using Quantum Annealing: an Empirical Study”
Marco Esposito (joint work with Benigno Ansanelli, Leonardo Picchiami): “Simulation-based Design of Critical Systems via Black-Box Optimization and Statistical Model Checking”
19:00 Social dinner

7 June

9:00-11:00 Session: Software engineering
Thomas Jensen: “Compositional reasoning about non-interference properties of procedures”
Chiara Braghin (joint work with Elvinia Riccobene and Simone Valentini): “A Formal Framework for correct-by-construction development of Ethereum Smart Contracts”
Cosimo Laneve (joint work with Giuseppe De Palma, Saverio Giallorenzo, Cosimo Laneve, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro): “Serverless Scheduling Policies based on Cost Analysis”
11:00-11:30 Coffe break
11:30-13:30 Session: Applications of program analysis and verification
Luca Pasetto “Challenges of Software Verification for the EU AI Act”
Marco De Vincenzi (joint work with Chiara Bodei, Gabriele Costa, Ilaria Matteucci and Dajiang Suo): “Security Analysis of a V2I Authentication Protocol”
Nicola Assolini (joint work with Alessandra Di Pierro and Isabella Mastroeni): “Uncomputing Quantum Variables: a Static Analysis”
Giacomo Zanatta (joint work with Gianluca Caiazza, Pietro Ferrara, Luca Negrini, Ruffin White): “Automating ROS2 Security Policies Extraction through Static Analysis”
13:30-15:00 Lunch break

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), publicity chair

Luca Negrini (University of Venice), web chair

Luca Olivieri (University of Venice), sponsorship chair

Important dates

All dates are tentative and might change in the future.

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