Programme

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

Monday 08 April

08:45
Opening
10:00
Coffee break
TACAS: SAT and SMT
Chair: Laura Kovács
Room: Hollenfels
10:30
Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes
11:00
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč
11:15
Md Solimul Chowdhury, Cayden Codel and Marijn Heule
11:30
Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel
12:00
Marijn Heule and Manfred Scheucher
TACAS: Synthesis
Chair: Bernd Finkbeiner
Room: Diekirch-Echternach-Fischbach
10:30
Rüdiger Ehlers and Ayrat Khalimov
11:00
Tom van Dijk, Feije van Abbema and Naum Tomov
11:30
S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty
12:00
Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer
FASE: Runtime Approaches
Chair: Reiner Hähnle
Room: Schengen II
11:00
Yliès Falcone, Gwen Salaün, and Ahang Zuo
12:00
Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon
Rust
Room: Schengen I
10:30
Tree Borrows
Neven Villani, Johannes Hostert, Ralf Jung and Derek Dreyer
11:00
Aeneas: Rust Verification by Functional Translation
Son Ho, Jonathan Protzenko and Aymeric Fromherz
11:30
Contracts for Rust
Felix Klock and Celina Val
12:00
Building User-Friendly Rust Verification Tools
Federico Poli
12:30
Lunch
TACAS: Proof Checking
Chair: Marijn Heule
Room: Hollenfels
14:00
Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury
14:30
Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov
15:00
Thibault Hilaire, David Ilcinkas and Jérôme Leroux
15:30
Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu
FASE: System Comprehension
Chair: Andrzej Wąsowski
Room: Schengen II
14:00
Margarita Capretto, Martin Ceresa, and Cesar Sanchez
14:30
Jan H. Boockmann, and Gerald Luettgen
15:00
Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang, and Guojun Ma
15:30
Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, and Zhiping Shi
Rust
Room: Schengen I
14:00
Verifiying a Concurrent Memory Allocator with Verus
Travis Hance
14:30
Efficiently Verifying Rust Traits with SMT Solvers
Chris Hawblitzel
15:00
OxiDD: Verification Challenge
Nils Husung, Clemens Dubslaff and Maximilian Alexander Köhl
15:30
Rust Verification Workshop Proposal: Crowdsourcing the Rust standard library verification
Celina G. Val and Rahul Kumar
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
14:00
Introduction to SV-COMP
Dirk Beyer
14:25
Bubaak (Marek Chalupa), Bubaak-SpLit (Cedric Richter), ConcurrentWitness2Test (Levente Bajczi), CPAchecker (Daniel Baier), CPV (Po-Chun Chien)
14:45
EmergenTheta (Zsófia Ádám), ESBMC (Rafael Sá Menezes), Goblint (Michael Schwarz), Goblint Validator (Simmo Saan)
15:00
Korn (Gidon Ernst), LIV (Marian Lingsch-Rosenfeld), Mopsa (Raphaël Monat), PredatorHP (Veronika Šoková), PROTON (Ravindra Metta), SWAT (Nils Loose), Symbiotic (Jan Strejček), Theta (Csanád Telbisz)
15:30
UAutomizer (Matthias Heizmann), UGemCutter (Dominik Klumpp), UKojak (Frank Schüssele), VeriAbsL (Priyanka Darke), Witch 3 (Paulína Ayaziová), WitnessLint (Marian Lingsch-Rosenfeld)
Diversity & Inclusion
Chair: Peter Roenne
Room: Europe A
14:00
Why do we talk about Equality and Diversity in research?
Inês Crisóstomo
14:10
The Computer Girls: Exploring Herstory
Valérie Schafer
14:50
Building an Inclusive Researcher Journey
Véronique Schlick
15:00
Interactive session and discussion
16:00
Coffee break
TACAS: Logic and Decidability
Chair: Sebastian Junges
Room: Hollenfels
17:00
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger
17:30
Laura Bocchi, Andy King and Maurizio Murgia
Invited Tutorial
Chair: Marieke Huisman
Room: Europe A
Rust
Room: Schengen I
16:30
Panel Discussion / Lightning Talks
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
16:30
Open SV-COMP Community Meeting

Tuesday 09 April

10:00
Coffee Break
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
11:30
Omar Al-Bataineh
11:45
Cedric Richter and Heike Wehrheim
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
10:30
Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck
11:00
Laurent Doyen, Pranshu Gaba and Shibashis Guha
11:30
Daniel Hausmann, Mathieu Lehaut and Nir Piterman
12:00
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
TACAS: Model Checking
Chair: Kristin Rozier
Room: Hollenfels
14:00
Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi
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:30
Jack Hughes and Dominic Orchard
FoSSaCS: Categorical semantics
Chair: Corina Cirstea
Room: Diekirch-Echternach-Fischbach
14:30
Alejandro Villoria, Henning Basold and Alfons Laarman
15:00
Fabian Birkmann, Stefan Milius and Henning Urbat
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
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:00
Loes Kruger, Sebastian Junges and Jurriaan Rot
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

Wednesday 10 April

10:00
Coffee Break
TACAS: Software Verification
Chair: Tomáš Vojnar
Room: Hollenfels
10:30
Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy
11:00
Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich
12:00
Leping Zhang, Yongwang Zhao and Jianxin Li
ESOP: Domain-Specific Languages
Chair: Josh Ko
Room: Schengen II
11:00
Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang
11:30
Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix
FoSSaCS: Automata and Synthesis
Chair: Bart Jacobs
Room: Diekirch-Echternach-Fischbach
11:30
Marek Jankola and Jan Strejček
12:00
Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy
Spin: Software Verification
Chair: Thomas Neele
Room: Schengen I
10:30
Taming the AI Monster: Monitoring of Individual Fairness for Effective Human Oversight (keynote)
Holger Hermanns
11:30
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants*
Dirk Beyer, Po-Chun Chien and Nian-Ze Lee
12:00
Max Barth and Marie-Christine Jakobs
12:30
Lunch
13:00
ETAPS General Assembly
TACAS: Probabilistic Systems
Chair: Kim Larsen
Room: Hollenfels
14:00
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler
14:30
Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen
15:00
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges
15:30
Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr
ESOP: Bidirectional typing / Session types
Chair: Ugo Dal Lago
Room: Schengen II
14:00
Liang-Ting Chen and Hsiang-Shang Ko
15:00
Luis Caires and Bernardo Toninho
15:30
Elaine Li, Felix Stutz and Thomas Wies
FoSSaCS: Types and Programming Languages
Chair: James Worrell
Room: Diekirch-Echternach-Fischbach
14:00
Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter
14:30
Beniamino Accattoli and Adrienne Lancelot
15:00
Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat
15:30
Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale
Spin: Anniversary Track
Chair: Anton Wijs
Room: Schengen I
14:00
The Spin on Spin (keynote)
Gerald Holzmann
15:00
Two Decades of Industrializing Formal Verification: The Reactis Story
Rance Cleaveland, David Hansel, Steve Sims and Scott Smolka
15:30
Automated Reasoning in Quantum Circuit Compilation
Dimitrios Thanos, Alejandro Villoria, Sebastiaan Brand, Arend-Jan Quist, Jingyi Mei, Tim Coopmans and Alfons Laarman
Tool demo session
Room: Europe B
14:00
16:00
Coffee break
TACAS: Simulations
Chair: Javier Esparza
Room: Hollenfels
17:00
Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski
17:30
Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo
ESOP: Dependent Types
Chair: Benoit Montagu
Room: Schengen II
16:30
Loïc Pujet and Nicolas Tabareau
17:00
Cyril Cohen, Enzo Crance and Assia Mahboubi
17:30
Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard
TACAS: Neural Networks
Chair: Arie Gurfinkel
Room: Diekirch-Echternach-Fischbach
16:30
Xiyue Zhang, Benjie Wang and Marta Kwiatkowska
17:00
Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer
17:30
Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt
Spin: Automated Reasoning
Chair: Alfons Laarman
Room: Schengen I
16:30
Random Access on Narrow Decision Diagrams in External Memory
Steffan Christ Sølvsten, Casper Moldrup Rysgaard and Jaco van de Pol
17:00
Solving Constrained Horn Clauses as C Programs with CHC2C
Levente Bajczi and Vince Molnár

Thursday 11 April

09:00
10:00
Coffee Break
TACAS: Testing and Verification
Chair: Ruzica Piskac
Room: Hollenfels
10:30
Lars B. van den Haak, Anton Wijs, Marieke Huisman and Mark van den Brand
11:00
Martin Jonáš, Jan Strejček, Marek Trtík and Lukáš Urban
11:30
Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jorgensen, Andreas Pavlogiannis and Jaco van de Pol
12:00
Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee and Nils Sirrenberg
ESOP: Verification and Analysis
Chair: Ori Lahav
Room: Schengen II
10:30
Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen
11:00
Sumanth Prabhu, Grigory Fedyukovich and Deepak D'Souza
11:30
Liye Guo and Cynthia Kop
12:00
Daniel Lundén, Lars Hummelgren, Jan Kudlicka, Oscar Eriksson and David Broman
FoSSaCS: Logic and Proofs
Chair: Ichiro Hasuo
Room: Diekirch-Echternach-Fischbach
10:30
Luca Geatti, Alessio Mansutti and Angelo Montanari
11:00
Philipp Czerner, Javier Esparza and Valentin Krasotin
11:30
Balder ten Cate and Jesse Comer
Spin: Verification Tools
Chair: Matthias Heizmann
Room: Schengen I
10:30
Learning the State Machine Behind a Modal Text Editor: The (Neo)Vim Case Study
Pierre Ganty
11:00
Tolerange: Quantifying Fault Masking in Stochastic Systems
Luciano Putruele, Ramiro Demasi, Pablo Castro and Pedro D'Argenio
11:30
Software Verification Witnesses 2.0
Paulína Ayaziová, Dirk Beyer, Marian Lingsch-Rosenfeld, Martin Spiessl and Jan Strejček
12:00
Fault Localization on Verification Witnesses*
Dirk Beyer, Matthias Kettl and Thomas Lemberger
12:30
Lunch
TACAS: Games
Chair: Bernd Finkbeiner
Room: Hollenfels
14:00
Guy Avni, Kaushik Mallik and Suman Sadhukhan
14:30
Satya Prakash Nayak and Anne-Kathrin Schmuck
15:00
Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci and Jaco van de Pol
15:30
Rupak Majumdar, Irmak Saglam and K. S. Thejaswini
ESOP: Verification
Chair: Luis Caires
Room: Schengen II
14:00
Yotam Dvir, Ohad Kammar and Ori Lahav
14:30
Léo Stefanesco, Azalea Raad and Viktor Vafeiadis
15:00
Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer and Brijesh Dongol
15:30
Shachar Itzhaky, Sharon Shoham and Yakir Vizel
FoSSaCS: Infinite-State Systems
Chair:: Jerome Leroux
Room: Diekirch-Echternach-Fischbach
14:00
Andrei Draghici, Christoph Haase and Andrew Ryzhikov
14:30
Jan-Christoph Kassing, Florian Frohn and Jürgen Giesl
15:00
Shaull Almagor, Guy Avni, Henry Sinclair-Banks and Asaf Yeshurun
Spin: Model Checking
Chair: Anton Wijs
Room: Ansembourg
14:00
MoXI: An Intermediate Language for Symbolic Model Checking (keynote)
Kristin Yvonne Rozier
15:00
Synchronisation in Language-level Symmetry Reduction for Probabilistic Model Checking
Ivaylo Valkov, Alastair Donaldson and Alice Miller
15:30
A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
Daisuke Ishii
Award Winner Presentations
Chair: Marieke Huisman
Room: Europe A
14:00
Doctoral Dissertation Award
Yotam Feldman: Towards a Theory of Learning Inductive Invariants
14:30
Test Of Time Award
Luca Cardelli and Andrew D. Gordon: Mobile Ambients
15:00
Test-Of-Time Tool Award
Marta Kwiatkowska, Gethin Norman, and David Parker: PRISM
15:30
Artifact Evaluation Report & Awards
Arnd Hartmanns, Hadar Frenkel, and Tobias Kappé
16:00
Coffee break
TACAS: Concurrency
Chair: Hadar Frenkel
Room: Hollenfels
16:30
Florian Furbach, Parosh Aziz Abdulla, Mohamed Faouzi Atig and Shashwat Garg
17:00
Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl
ESOP: Abstract Interpretation
Chair: Thomas Wies
Room: Schengen II
16:30
Sven Keidel, Dominik Helm, Tobias Roth and Mira Mezini
17:00
Raphaël Monat, Aymeric Fromherz and Denis Merigoux
Competition on Software Testing (Test-Comp)
Chair: Dirk Beyer
Room: Schengen I
16:30
Introduction to Test-Comp
Dirk Beyer
16:50
CoVeriTest (Marie-Christine Jakobs), ESBMC (Rafael Sá Menezes), FuSeBMC (Rafael Sá Menezes), Fizzer (Lukáš Urban), Utestgen (Max Barth)
17:40
Discussion
Programme in PDF for print

Accepted Papers

ESOP
  • Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer and Brijesh Dongol. Intel PMDK Transactions: Specification and Concurrency
  • Léo Stefanesco, Azalea Raad and Viktor Vafeiadis. Specifying and Verifying Persistent Libraries
  • Sumanth Prabhu, Grigory Fedyukovich and Deepak D’Souza. Maximal Quantified Precondition Synthesis for Linear Array Loops
  • Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen. Verified Inlining and Specialisation for PureCake
  • Liye Guo and Cynthia Kop. Higher-Order LCTRSs and Their Termination
  • Liang-Ting Chen and Hsiang-Shang Ko. A Formal Treatment of Bidirectional Typing
  • Jack Hughes and Dominic Orchard. Program Synthesis from Graded Types
  • Jason Z. S. Hu and Brigitte Pientka. Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis
  • Sven Keidel, Dominik Helm, Tobias Roth and Mira Mezini. A Modular Soundness Theory for the Blackboard Analysis Architecture
  • Cyril Cohen, Enzo Crance and Assia Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence
  • Raphaël Monat, Aymeric Fromherz and Denis Merigoux. Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
  • Hiroya Fujinami and Ichiro Hasuo. Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
  • Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni. Monadic Intersection Types, Relationally
  • Andrea Colledan and Ugo Dal Lago. Circuit Width Estimation via Effect Typing and Linear Dependency
  • Daniel Lundén, Lars Hummelgren, Jan Kudlicka, Oscar Eriksson and David Broman. Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
  • Shachar Itzhaky, Sharon Shoham and Yakir Vizel. Hyperproperty Verification as CHC Satisfiability
  • Théo Laurent, Meven Lennon-Bertrand and Kenji Maillard. Definitional Functoriality for Dependent (Sub)Types
  • Anders Ågren Thuné, Kazutaka Matsuda and Meng Wang. Reconciling Partial and Local Invertibility
  • Loïc Pujet and Nicolas Tabareau. Observational Equality Meets CIC
  • Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix. On the Hardness of Analyzing Quantum Programs Quantitatively
  • Yotam Dvir, Ohad Kammar and Ori Lahav. A Denotational Approach to Release-Acquire Concurrency
  • Pierre Lermusiaux and Benoit Montagu. Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
  • Thiago Felicissimo. Generic Bidirectional Typing for Dependent Type Theories
  • Sam Lindley, Cristina Matache, Sean Moss, Sam Staton, Nicolas Wu and Zhixuan Yang. Scoped Effects as Parameterized Algebraic Theories
  • Elaine Li, Felix Stutz and Thomas Wies. Deciding Subtyping for Asynchronous Multiparty Sessions
  • Luis Caires and Bernardo Toninho. The Session Abstract Machine
FASE
  • Lucas Sakizloglou, Holger Giese and Leen Lambers. Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
  • Margarita Capretto, Martin Ceresa and Cesar Sanchez. Monitoring the Future of Smart Contracts
  • Omar Al-Bataineh. Invariant-based Program Repair
  • Jan H. Boockmann and Gerald Luettgen. Comprehending Object State via Dynamic Class Invariant Learning
  • Yliès Falcone, Gwen Salaün and Ahang Zuo. Probabilistic Runtime Enforcement of Executable BPMN Processes
  • Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg and Mariëlle Stoelinga. Fuzzy quantitative attack tree analysis
  • Cedric Richter and Heike Wehrheim. Can ChatGPT support software verification?
  • Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang and Zhiping Shi. Refinement Verification of OS Services based on a Verified Preemptive Microkernel
  • He Xu, Sven Schneider and Holger Giese. Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems
  • Téo Bernier, Yani Ziani, Nikolai Kosmatov and Frédéric Loulergue. Combining Deductive Verification with Shape Analysis
  • Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho and Ruben Martins. Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation
  • Geunyeol Yu, Seunghyun Chae, Kyungmin Bae and Sungkun Moon. Formal Specification of Trusted Execution Environment APIs
  • Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang and Guojun Ma. Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data
  • Dré van Oorschot, Marieke Huisman and Ömer Şakar. First Steps towards Deductive Verification of LLVM IR
FoSSaCS
  • Pete Austin, Sougata Bose and Patrick Totzke. Parity Games on Temporal Graphs
  • Philip Saville. Clones, Closed Categories, and Combinatory Logic
  • Bart Jacobs. Drawing from an Urn is Isometric
  • Patrick Baillot, Ugo Dal Lago, Cynthia Kop and Deivid Vale. On Basic Feasible Functionals and the Interpretation Method
  • Andrei Draghici, Christoph Haase and Andrew Ryzhikov. Reachability in Fixed VASS: Expressiveness and Lower Bounds
  • Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck. Fair Omega-regular Games
  • Orna Kupferman, Ofer Leshkowitz and Naama Shamash Halevy. Synthesis with Privacy Against an Observer
  • Dario Stein and Richard Samuelson. Towards a Compositional Framework for Convex Analysis (with Applications to Probability Theory)
  • Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas and Henning Urbat. Logical Predicates in Higher-Order Mathematical Operational Semantics
  • Fabian Birkmann, Stefan Milius and Henning Urbat. Monoidal Extended Stone Duality
  • Jesse Comer and Balder ten Cate. Craig Interpolation for Decidable First-Order Fragments
  • Beniamino Accattoli and Adrienne Lancelot. Light Genericity
  • Jan-Christoph Kassing, Florian Frohn and Jürgen Giesl. From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
  • Valentin Blot, Gilles Dowek, Thomas Traversié and Théo Winterhalter. From Rewrite Rules to Axioms in the lambdaPi-Calculus Modulo Theory
  • Laurent Doyen, Pranshu Gaba and Shibashis Guha. Stochastic Window Mean-payoff Games
  • Lucie Guillou, Corto Mascle and Nicolas Waldburger. Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
  • Philipp Czerner, Javier Esparza and Valentin Krasotin. A Resolution-Based Interactive Proof System for UNSAT
  • Luca Geatti, Alessio Mansutti and Angelo Montanari. Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems
  • Alejandro Villoria, Henning Basold and Alfons Laarman. Enriching Diagrams with Algebraic Operations
  • Daniel Hausmann, Mathieu Lehaut and Nir Piterman. Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
  • Shaull Almagor and Neta Dafni. Determinization of Integral Discounted-Sum Automata is Decidable
  • Shaull Almagor, Guy Avni, Henry Sinclair-Banks and Asaf Yeshurun. Dimension-Minimality and Primality of Counter Nets
  • Aditya Prakash. Checking History-Determinism is NP-hard for Parity Automata
  • Marek Jankola and Jan Strejček. Tighter Construction of Tight Büchi Automata
TACAS

Regular Research Papers

  • Mayank Solanki, Prantik Chatterjee, Akash Lal and Subhajit Roy. Accelerated Bounded Model Checking Using Interpolation Based Summaries
  • Satya Prakash Nayak and Anne-Kathrin Schmuck. Most General Winning Secure Equilibria Synthesis in Graph Games
  • Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot and Sebastian Junges. Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
  • Marijn Heule and Manfred Scheucher. Happy ending: An empty hexagon in every set of 30 points
  • Leonardo Lima, Jonathan Huerta Y Munive and Dmitriy Traytel. Explainable Online Monitoring of Metric First-Order Temporal Logic
  • Yubo Cai and Gleb Pogudin. Dissipative quadratizations of polynomial ODE systems
  • S. Akshay, Eliyahu Basa, Dror Fried and Supratik Chakraborty. On Dependent Variables in Reactive Synthesis
  • Lukas Westhofen, Christian Neurohr, Daniel Neider and Jean Christoph Jung. Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
  • Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
  • Xiyue Zhang, Benjie Wang and Marta Kwiatkowska. Provable Preimage Under-Approximation for Neural Networks
  • Laura Bocchi, Andy King and Maurizio Murgia. Asynchronous Subtyping by Trace Relaxation
  • Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist. Scalable Tree-based Register Automata Learning
  • Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu. A Logical Treatment of Finite Automata
  • Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán and Yon Shin Teo. A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
  • Abhishek Kr Singh and Ori Lahav. Decidable Verification under Localized Release-Acquire Concurrency
  • Antonio Jiménez-Pastor, Kim Guldstrand Larsen, Mirco Tribastone and Max Tschaikowski. Forward and Backward Constrained Bisimulations for Quantum Circuits
  • Rüdiger Ehlers and Ayrat Khalimov. Fully Generalized Reactivity(1) Synthesis
  • Aditi Kabra, Jonathan Laurent, Stefan Mitsch and André Platzer. CESAR: Control Envelope Synthesis via Angelic Refinements
  • Raven Beutner. Automated Software Verification of Hyperliveness
  • Martin Jonáš, Jan Strejček, Marek Trtík and Lukáš Urban. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
  • Muhammad Osama and Anton Wijs. Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
  • Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger. Deciding Boolean Separation Logic via Small Models
  • Rupak Majumdar, Irmak Saglam and K. S. Thejaswini. Rabin Games and Colourful Universal Trees
  • Loes Kruger, Sebastian Junges and Jurriaan Rot. Small Test Suites for Active Automata Learning
  • Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr. Learning Explainable and Better Performing Representations of POMDP Strategies
  • Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou. Formally verified asymptotic consensus in robust networks
  • Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jorgensen, Andreas Pavlogiannis and Jaco van de Pol. Fast Symbolic Computation of Bottom SCCs
  • Guy Avni, Kaushik Mallik and Suman Sadhukhan. Auction-Based Scheduling
  • Dong Xu, Nusrat Jahan Mozumder, Hai Duong and Matthew Dwyer. Training for Verification: Increasing Neuron Stability to Scale DNN Verification
  • Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike and John Backes. DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
  • Florian Furbach, Parosh Aziz Abdulla, Mohamed Faouzi Atig and Shashwat Garg. Verification under TSO with an infinite Data Domain
  • Sumanth Prabhu, Deepak D’Souza, Supratik Chakraborty, Venkatesh R and Grigory Fedyukovich. Weakest Precondition Inference for Non-Deterministic Linear Array Programs
  • Hari Govind Vediramana Krishnan, Isabel Garcia-Contreras, Sharon Shoham and Arie Gurfinkel. Speculative SAT modulo SAT
  • Thibault Hilaire, David Ilcinkas and Jérôme Leroux. A State-of-the-Art Karp-Miller Algorithm Certified in Coq
  • Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga and Nils Jansen. CTMCs with Imprecisely Timed Observations

Case Study Papers

  • Lukas Koenig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kueperkoch, Dennis Fassbender and Michael Hanselmann. Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
  • Leping Zhang, Yongwang Zhao and Jianxin Li. A Comprehensive Specification and Verification of the L4 Microkernel API
  • Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler and Sascha Witt. Formally Verifying an Efficient Sorter

Tool Demo Papers

  • Md Solimul Chowdhury, Cayden Codel and Marijn Heule. TaSSAT: Transferring and Sharing in SAT
  • Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč. Z3-Noodler: An Automata-based String Solver
  • Mertcan Temel. VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
  • Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov. Automate where Automation Fails: Proof Strategies for Frama-C/WP

Regular Tool Papers

  • Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci and Jaco van de Pol. On-The-Fly Algorithm for Reachability in Parametric Timed Games
  • Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee and Nils Sirrenberg. Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
  • Matthias Cosler, Christopher Hahn, Ayham Omar and Frederik Schmitt. NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
  • Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl. OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust
  • Michalis Kokologiannakis, Viktor Vafeiadis and Rupak Majumdar. Enhancing GenMC’s Usability and Performance
  • David Chocholatý, Tomas Fiedor, Vojtěch Havlena, Lukáš Holík, Martin Hruska, Ondrej Lengal and Juraj Síč. Mata: A Fast and Simple Finite Automata Library
  • Tom van Dijk, Feije van Abbema and Naum Tomov. Knor: reactive synthesis using Oink
  • Cyrille Valentin Artho, Pavel Parizek, Daohan Qu, Varadraj Galgali and Pu Yi. JPF: From 2003 to 2023
  • Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo and Dongjie He. SootUp: A Redesign of the Soot Static Analysis Framework
  • Lars B. van den Haak, Anton Wijs, Marieke Huisman and Mark van den Brand. HaliVer: Deductive Verification and Scheduling Languages Join Forces
  • Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury. IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL