Log in | Join us

Programme

Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.

Monday Tuesday Wednesday Thursday

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
Fuzzy quantitative attack tree analysis
Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, and Mariëlle Stoelinga
11:00
Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation
Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho, and Ruben Martins
11:30
Invariant-based Program Repair
Omar Al-Bataineh
11:45
Can ChatGPT support software verification?
Cedric Richter and Heike Wehrheim
12:00
Combining Deductive Verification with Shape Analysis
Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue
12:15
First Steps towards Deductive Verification of LLVM IR
Dré van Oorschot, Marieke Huisman, and Ömer Şakar
TACAS: Program Analysis and Proofs
Chair: Andrei Voronkov
Room: Hollenfels
10:30
SootUp: A Redesign of the Soot Static Analysis Framework
Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He
11:00
Formally verified asymptotic consensus in robust networks
Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou
11:30
Formally Verifying an Efficient Sorter
Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt
12:00
Explainable Online Monitoring of Metric First-Order Temporal Logic
Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel
FoSSaCS: Infinite games
Chair: Shaull Almagor
Room: Diekirch-Echternach-Fischbach
10:30
Fair Omega-regular Games
Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck
11:00
Stochastic Window Mean-payoff Games
Laurent Doyen, Pranshu Gaba and Shibashis Guha
11:30
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
Daniel Hausmann, Mathieu Lehaut and Nir Piterman
12:00
Parity Games on Temporal Graphs
Pete Austin, Sougata Bose and Patrick Totzke
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
JPF: From 2003 to 2023
Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi
14:30
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
Muhammad Osama and Anton Wijs
15:00
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann
15:30
Enhancing GenMC's Usability and Performance
Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar
ESOP: Effects and Modal Types
Chair: Kazutaka Matsuda
Room: Schengen II
14:00
Scoped Effects as Parameterized Algebraic Theories
Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang
14:30
Monadic Intersection Types, Relationally*
Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni
15:00
Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
Jason Z. S. Hu and Brigitte Pientka
15:30
Program Synthesis from Graded Types
Jack Hughes and Dominic Orchard
FoSSaCS: Categorical semantics
Chair: Corina Cirstea
Room: Diekirch-Echternach-Fischbach
14:00
Drawing from an Urn is Isometric
Bart Jacobs
14:30
Enriching Diagrams with Algebraic Operations
Alejandro Villoria, Henning Basold and Alfons Laarman
15:00
Monoidal Extended Stone Duality
Fabian Birkmann, Stefan Milius and Henning Urbat
15:30
Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
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
Scalable Tree-based Register Automata Learning*
Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist
17:00
Small Test Suites for Active Automata Learning
Loes Kruger, Sebastian Junges and Jurriaan Rot
17:30
Mata: A Fast and Simple Finite Automata Library
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
16:30
Tamar Sharon: The view from ethics: What technologies promise, what they do and who benefits
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
Programme in PDF for print
Full Programme

ETAPS Association

Internal

Responsible for these web pages:

Jan Kofroň
Faculty of Mathematics and Physics
Charles University, Czech Republic
E-mail: firstname.lastname [at] d3s.mff.cuni.cz
Phone: +420 951 554 285