May 25-26, 2023, Venice, Italy

Following the success of the first CSV workshop in 2022, the Symposium on “Challenges of Software Verification” will take place on Thursday 25th and Friday 26th May 2023 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 has been published in Springer-Nature

Pictures of CSV 2023


Schedule

25 May

10:45-11:00 Welcome
11:00-13:00 Session: Abstract Interpretation
Chair: Francesco Parolini (Sorbonne University, France)
Denis Mazzucato (INRIA Paris – joint work with Marco Campion and Caterina Urban): “Quantitative Input Feature Usage” [SLIDES]
Michele Pasqua (University of Verona): “Static Analysis Properties as Program Hyperproperties” [SLIDES]
Isabella Mastroeni (University of Verona): “A General Model for Semantics Input/Output Dependencies” [SLIDES]
Helmut Seidl (TU Munich – joint work with Michael Schwarz and Julian Erhard): “Weakly Relational Domains” [SLIDES]
13:00-14:00 Lunch break
14:00-16:00 Session: Software Engineering
Chair: Pietro Ferrara (Ca’ Foscari University of Venice, Italy)
Giulia Sellitto (University of Salerno – joint work with Vincenzo De Martino, Dario Di Nucci, Filomena Ferrucci, Fabio Palomba): “Investigating the Role of Hyper-Parameter Tuning and Algorithm Selection on the Performance of Mobile App Energy Consumption Optimization” [SLIDES]
Kevin De Porre (VUB – joint work with Carla Ferreira and Elisa Gonzalez Boix): “Verification of Replicated Data Types using VeriFx” [SLIDES]
Davide Corradini (University of Verona – joint work with Michele Pasqua, Mariano Ceccato): “Challenges in Automated Black Box Test Case Generation for REST APIs”
Davide Taibi (Tampere University): “Testing in the cloud: issues and solutions” [SLIDES]
16:00-16:30 Coffe break
16:30-18:30 Session: Security
Chair: Gianluca Caiazza (Ca’ Foscari University of Venice, Italy)
Riccardo Scandariato (TU Hamburg – joint work with Simon Schneider and Katja Tuma): “Static analysis for modern applications: a security perspective” [SLIDES]
Marco De Vincenzi (IIT – joint work with Chiara Bodei and Ilaria Matteucci): “Security verification of an automotive solution” [SLIDES]
Luca Olivieri (University of Verona and Corvallis SRL – joint work with Fausto Spoto): “Software Verification Challenges in Blockchain”
Mariano Ceccato (University of Verona – joint work with Alberto Lovato, Niccolò Marastoni): “Remote Software Verification with Next Generation Secure IoT Processors”
19:00 Social dinner

26 May

9:00-10:30 Session: Static analysis in practice
Chair: Agostino Cortesi (Ca’ Foscari University of Venice, Italy)
Roberto Bagnara (University of Parma and Bugseng – joint work with Abramo Bagnara, Federico Serafini): “C-rusted: The Advantages of Rust, in C, without the Disadvantages” [SLIDES]
Laura Titolo (NASA – joint work with Mariano Moscato, Marco Feliu, Aaron Dutle): “ReFlow: from real number specifications to verified floating-point implementations” [SLIDES]
Jorge A Navas (Certora): “Verification of Solana programs using the Certora Prover” [SLIDES]
10:30-11:00 Coffe break
11:00-12:30 Session: Theoretical aspects of static analysis
Chair: Helmut Seidl (TU Munich, Germany)
David Monniaux (University of Grenoble Alpes, CNRS – joint work with Benjamin Bonneau, Sylvain Boulme, Leo Gourdin): “Formally verified static analysis in formally verified compilation” [SLIDES]
Thomas Jensen (INRIA Rennes): “A PER logic of information flow” [SLIDES]
Linda Brodo (University of Sassari – joint work with Moreno Falaschi,Valeria Montagna, Pasquale Pulieri, Roberto Bruni, Roberta Gori, and Paolo Milazzo): “Analysis of Positive Reaction Systems” [SLIDES]

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, Corvallis SRL), web chair

Luca Olivieri (University of Verona, Corvallis SRL), sponsorship chair

Important dates

  • February 28: deadline for abstract submissions
  • March 15: acceptance notification
  • April 20: symposium registration
  • May 25-26: symposium
  • July 31: full version for special issue submission

Sponsors