Program
Important: All presentations will be held in the Aula Prima (Wednesday to Friday). Please consult here for venue directions. Details on the respective workshop programmes can be found here.
Tuesday, November 24
| Time | Session | Details |
|---|---|---|
| 18:00 – 20:00 | Welcome Reception | First floor (registration will be open) |
Wednesday, November 25
| Time | Session | Details | Authors |
|---|---|---|---|
| 08:00 – 09:00 | Registration | First floor | |
| 09:00 – 10:00 | Invited Talk | Reading Between the Lines of Code | Elizabeth Polgreen |
| 10:00 – 10:30 | Coffee break | Second Floor | |
| 10:30 – 11:00 | AI and Machine Learning Verification | Functional Basis Reduction of Neural Networks via Approximate Hidden-Neuron Lumping | Ravi Dhiman, Andrea Passarella, Mirco Tribastone and Lorenzo Valerio |
| 11:00 – 11:30 | AI and Machine Learning Verification | Discovering Markovian Models from Event Logs for Resource-Aware Process Analysis | Carlos E. Budde, Vlad Paul Cosma, Alyzia Konsta and Hugo A. López |
| 11:30 – 12:00 | AI and Machine Learning Verification | Another Brick in the Loop: From Graphical Loop Invariant to Formal Proofs | Géraldine Brieven, Antoine Grosjean, Pascal Fontaine and Benoit Donnet |
| 12:00 – 12:30 | AI and Machine Learning Verification | Reactive Correspondence Relationships for Incremental Triple Graph Grammar-Style Model Synchronisation | Monalisha Ojha, Shilpi Gupta, Mohammad Sadeghi, Colin Atkinson, Sebastian Bergemann, Derui Zhu and Alexander Pretschner |
| 12:30 – 13:30 | Lunch | Second Floor | |
| 13:30 – 14:00 | Security, Safety and Dependable Systems | A Formal Case Study of Side-Channel Attacks on a Water Supply System | Julian Klein and Sabine Glesner |
| 14:00 – 14:30 | Security, Safety and Dependable Systems | Formally Verifying Noir Zero Knowledge Programs with NAVe | Pedro Antonino and Namrata Jain |
| 14:30 – 15:00 | Security, Safety and Dependable Systems | SMAC: A Calculus for Verifying Memory Arrays in Isabelle/Solidity | Diego Marmsoler and Asad Ahmed |
| 15:00 – 15:30 | Coffee break | Second Floor | |
| 15:30 – 16:00 | Formal Verification and Program Reasoning | Verifying Numerical Methods with Isabelle/HOL | Dustin Bryant, Jonathan Julian Huerta Y Munive and Simon Foster |
| 16:00 – 16:30 | Formal Verification and Program Reasoning | Modular Composition of Inductive Types Using Lean Meta-programming | Ramy Shahin |
| 16:30 – 17:00 | Formal Verification and Program Reasoning | Verifying a Rust Bitmap Allocator in RocQ | Rahul Sankalana Gunawardhana, Narges Khakpour and Conrad Grobler |
| 17:00 – 17:30 | Formal Verification and Program Reasoning | Practical Range Refinement Types with Inference | Valentin Aebi and Carlo A. Furia |
Thursday, November 26
| Time | Session | Details | Authors |
|---|---|---|---|
| 09:00 – 10:00 | Invited Talk | From Intent to Guarantees: Building Trustworthy Software Systems | Dalal Alrajeh |
| 10:00 – 10:30 | Coffee break | Second Floor | |
| 10:30 – 11:00 | Testing, Monitoring and Assurance | Integrating Parallel Trace Abstraction and Explicit Exploration for Test-Case Generation | Max Barth and Marie-Christine Jakobs |
| 11:00 – 11:30 | Testing, Monitoring and Assurance | Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers | Rosa Abbasi and Eva Darulova |
| 11:30 – 12:00 | Testing, Monitoring and Assurance | Diverse Counterexample Pools for Hybrid Automata: Generation and Selection | Sergio Quijano, József Kovács, Georg Arapatsakos, Erika Ábrahám, Mahsa Varshosaz and Andrzej Wasowski |
| 12:00 – 12:30 | Testing, Monitoring and Assurance | Revisiting Sequentialization of Concurrent C Programs | Dirk Beyer, Noah Koenig and Marian Lingsch-Rosenfeld |
| 12:30 – 13:30 | Lunch | Second Floor | |
| 13:30 – 14:00 | Security, Safety and Dependable Systems | Robust Skill Execution for Autonomous Robots | Pierre Malafosse, Alexandre Albore, David Doose, Jérémie Guiochet and Charles Lesire |
| 14:00 – 14:30 | Security, Safety and Dependable Systems | Formal Verification of a Blockchain-Based Healthcare Consent Management Protocol | Suraj Gupta, Frédéric Lang, Umar Ozeer and Gwen Salaün |
| 14:30 – 15:00 | Security, Safety and Dependable Systems | Protecting Sensitive Data Against Deductions in Business Processes: Formal Semantics and Model-Checking | Vincent Hugot, Sabine Frittella and Amine Rifi |
| 15:00 – 15:30 | Coffee break | Second Floor | |
| 15:30 – 16:00 | Testing, Monitoring and Assurance | Runtime Verification of Communicating Systems Using Data-Aware Interaction Models and Broker-Based Observations | Darine Rammal, Chana Weil-Kennedy, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, Pascale Le Gall, Erwan Mahe, Maxime Morin and Abdelaziz Ouazzani Chahidi |
| 16:00 – 16:30 | Testing, Monitoring and Assurance | Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring | Daisuke Ishii |
| 16:30 – 17:00 | Testing, Monitoring and Assurance | Policy-Guided Test Generation for Autonomous Driving Systems via Probabilistic Model Checking | Srajan Goyal, Radu Calinescu, Alberto Griggio, Ioannis Stefanakos and Stefano Tonetta |
| 17:00 – 17:30 | Testing, Monitoring and Assurance | Formal Verification of Stability in Provisioning Changes with BPlan | Eloi Perdereau, Daniel Sokolowski, Jolan Philippe, Hélène Coullon and Guido Salvaneschi |
Friday, November 27
| Time | Session | Details | Authors |
|---|---|---|---|
| 08:40 – 09:00 | Short Papers and Tool Papers | Don’t Blame the Model, Verify the Data: An Evaluation of SMT-based Dataset Verification | Sehee Park, Dominik Geißler, Andrei Aleksandrov and Kim Völlinger |
| 09:00 – 09:30 | Short Papers and Tool Papers | Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python | Akira Tanaka and Yusuke Kawamoto |
| 09:30 – 10:00 | Short Papers and Tool Papers | KeY4CATs: A Deductive Verification Tool for Context-aware Trace Contracts | Marco Scaletta |
| 10:00 – 10:30 | Coffee break | Second Floor | |
| 10:30 – 11:00 | Formal Verification and Program Reasoning | Borderlines of Soundness: Verifying C Aliasing Properties | Jérémy Damour, Loïc Correnson, Frédéric Loulergue and Allan Blanchard |
| 11:00 – 11:30 | Formal Verification and Program Reasoning | Encodability Criteria for Labelled Semantics | Lukas Bartl, Cinzia Di Giusto and Kirstin Peters |
| 11:30 – 12:00 | Formal Verification and Program Reasoning | Efficient Verification of C Programs with Pointers, Structs, and Arrays | Alexander Stekelenburg and Marieke Huisman |
| 12:00 – 12:30 | Formal Verification and Program Reasoning | PETRIFY: Petri-net Based Analysis of Concurrency Properties in Java Bytecode | Akshatha Shenoy and Carlo A. Furia |
| 12:30 – 13:30 | Lunch | Second Floor | |
| 13:30 – 14:00 | Security, Safety and Dependable Systems | Verification of a Configurable Railway Protection System: Pushing the Envelope | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi, Giuseppe Scaglione and Dylan Trenti |
| 14:00 – 14:30 | Security, Safety and Dependable Systems | Automated Abstraction Refinement for Information Flow Security in Embedded Systems | Jonas Becker-Kupczok, Lukas Ernst and Paula Herber |
| 14:30 – 15:00 | Security, Safety and Dependable Systems | Formal Verification of Credential Provisioning in ISO 15118 Park-and-Charge and Introducing Secure Ownership Transfer | Gabriele Bellini and Roberto Metere |
| 15:00 – 15:30 | Coffee break | Second Floor | |
| 15:30 – 16:00 | Formal Verification and Program Reasoning | Automata-Guided Local Proof Obligations for Temporal Safety in Synchronous Programs | Térence Clastres and Frédéric Dabrowski |
| 16:00 – 16:30 | AI and Machine Learning Verification | Bridging the Integration Bottleneck: A Java Architecture for Model Checking-Guided Reinforcement Learning | Ahmed Nagy Abdelkhalek Mansour, Samuele Grillo, Matteo Rossi and Vincenzo Viscusi |
| 16:30 – 17:00 | AI and Machine Learning Verification | Navigating the Random Forest: Verifying ML Models in Safety-Critical Applications with SMT Solvers | Iwo Kurzidem, Nina Vucenovic, Jakob Schleicher, Karsten Roscher and Dirk Beyer |
| 17:00 – 17:30 | AI and Machine Learning Verification | The Scaffolding Paradox: Evidence from AI-Assisted Dafny Proof Synthesis | Anastasiya Kravchuk-Kirilyuk, Dat Nguyen, Rhea Karty, Simon Henniger, Gabriel Poesia and Nada Amin |
Edit the content of this page here.