Programme
Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.
Tuesday 09 April
09:00
Sandrine Blazy: From Operational Semantics to Verified Compilation (unifying speaker)
Chair: Stephanie Weirich
Room: Europe A
10:00
Coffee Break
Room: Europe C
FASE: Fuzzing and NIER
Chair: Dirk Beyer
Room: Schengen II
10:30
Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, and Mariëlle Stoelinga
11:00
Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho, and Ruben Martins
12:00
Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue
12:15
Dré van Oorschot, Marieke Huisman, and Ömer Şakar
TACAS: Program Analysis and Proofs
Chair: Andrei Voronkov
Room: Hollenfels
10:30
Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He
11:00
Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou
11:30
Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt
12:00
Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel
FoSSaCS: Infinite games
Chair: Shaull Almagor
Room: Diekirch-Echternach-Fischbach
11:30
Daniel Hausmann, Mathieu Lehaut and Nir Piterman
Industry Day
Room: Wiltz
10:30
Invited talk: Formal Verification of Avionics Software
David Delmas (Airbus Operations SAS)
11:00
Collision-Free Trajectories in Automated Driving: Extending a Formal Argumentation From Single Scenarios to Scenario Ranges
Franziska Henze (CARIAD SE)
11:20
[11:20] How Bosch Brings Formal Methods to Autonomous Systems Engineering
Michaela Klauck (Robert Bosch GmbH), Christian Heinzemann and Ralph Lange
11:40
[11:40] Invited talk: European R&D Projects: Participation and Opportunities
Leonardo Tonetto (Advisor ‑ European R&D and Innovation Support)
12:15
[12:15] Networking Session
Each participant can present a 1-minute no-slide pitch about their interests in collaboration
Rust
Room: Schengen I
10:30
A hybrid approach to semi-automated Rust verification
Xavier Denis and Sacha-Elie Ayoun
11:00
Advances in the Rust compiler to ease the development of verification tools
Celina G. Val and Oli Scherer
11:30
Towards sound journeys through unsafe areas riding VeriFast
Nima Rahimi Foroushaani and Bart Jacobs
12:00
Refinement Proofs in Rust using Ghost Locks
Aurel Bílý
12:30
Lunch
Room: Europe B
TACAS: Model Checking
Chair: Kristin Rozier
Room: Hollenfels
14:00
Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi
14:30
Muhammad Osama and Anton Wijs
15:00
Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann
15:30
Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar
ESOP: Effects and Modal Types
Chair: Kazutaka Matsuda
Room: Schengen II
14:00
Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang
14:30
Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni
15:00
Jason Z. S. Hu and Brigitte Pientka
FoSSaCS: Categorical semantics
Chair: Corina Cirstea
Room: Diekirch-Echternach-Fischbach
14:30
Alejandro Villoria, Henning Basold and Alfons Laarman
15:30
Dario Stein and Richard Samuelson
Industry Day
Room: Wiltz
14:00
Invited talk: Next Generation Model-based Testing for Industrial Applications
Jan Peleska (Verified Systems International)
14:30
Invited talk: What Programmers Want from Proof with SPARK
Yannick Moy (AdaCore)
15:00
Retrospective on Formal Verification of a JavaCard Virtual Machine with Frama-C
Adel Djoudi (Thales Digital Identity & Security)
15:20
[15:20] Formal Methods in the Railways: Trajectory and Trends
Thierry Lecomte (Clearsy), Sébastien Agostini, David Déharbe, Julien Molinéro-Pérez, Erwan Mottin and Denis Sabatier
15:40
[15:40] Recommended Practice on Assurance of AI-enabled systems
Odd Ivar Haugen (DNV)
Rust
Room: Schengen I
14:00
How to do modular verification of Rust programs using Kani – Tool Demo
Justus Adam, Felipe Monteiro and Celina Val
14:30
Concolic Execution for Mid-level Intermediate Representation of Rust Programs
Mohammad Omidvar Tehrani, Tan Khang Le, Frédéric Tuong and Steven Y. Ko
15:00
HACL-rs: A Verified Rust Cryptographic Library
Aymeric Fromherz, Jonathan Protzenko and Son Ho
15:30
Hax - Enabling High Assurance Cryptographic Software
Franziskus Kiefer, Karthikeyan Bhargavan, Lucas Franceschino, Lasse Letager Hansen, Jonas Schneider-Bensch and Bas Spitters
Ask-me-anything
Room: Europe A
14:00
On Ethics, AI and Programming with Tamar Sharon and Wolfgang Ahrendt
Host: Tom van Dijk
15:00
Putting Science on the Political Agenda with Ana Cavalcanti and Gerald Lüttgen
Host: Sebastian Junges
16:00
Coffee break
Room: Europe C
TACAS: Automata and Learning
Chair: Anne-Kathrin Schmuck
Room: Hollenfels
16:30
Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist
17:30
David Chocholatý, Tomas Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruska, Ondrej Lengal and Juraj Síč
Invited Tutorial
Chair: Lenore Zuck
Room: Europe A
Industry Day
Room: Wiltz
16:30
Invited talk: From Theory to Practice: What is a contract, really?
Fritz Henglein (Deon Digital)
17:00
Formal Methods in Web3: Success Stories and Opportunities
Franck Cassez (Mantle Research)
17:20
[17:20] Securing the Aptos Framework through formal verification with the Move Prover
Wolfgang Grieskamp (Aptos Labs), Junkil Park and Teng Zhang
17:40
[17:40] Experience Report: Formally Verifying Critical Blockchain Network Component
Bhargav Bhatt (Web3 Foundation)
Rust
Room: Schengen I
16:30
Panel Discussion