Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Monday 13 April
08:45
ETAPS 2026 Opening
Chair: Laura Kovács
Room: Sala 500
09:00
Christel Baier: Verification of Infinite-horizon Properties of Dynamic Bayesian Networks
Chair: Nathalie Bertrand
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Proofs and Quantifier Elimination
Chair: Naijun Zhan
Room: Sala 500
10:30
Dominik Schreiber, Mathias Fleury, Katalin Fazekas and Armin Biere.
10:50
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli.
11:50
Peter Pfeiffer, Mark Peyrer, Daniel Grosse and Martina Seidl.
12:00
Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin and Georg Zetzsche.
12:10
Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan.
FASE: SE and AI
Chair: Elvira Albert and Corina Pasareanu
Room: Sala Madrid
10:30
Monika Gupta, Ajay Meena, Anamitra Roy Choudhury, Vijay Arya and Srikanta Bedathur.
10:50
Erin Woo, Sangyeop Yeo, Hyungkook Jun, Sangcheol Kim, Seung-won Hwang and Yu-Seung Ma.
11:10
Yili Jiang, Zhuoran Yan, Ning Ge, Yuan Wang, Jiahao Weng and Chunming Hu.
11:30
Giacomo Fantino, Marco Rondina, Antonio Vetro' and Juan Carlos De Martin.
11:50
Imane Bousdira, Martin Cooper and Aurélie Hurault.
12:10
Olivier Zeyen, Karim Tit, Maxime Cordy and Gilles Perrouin.
FOSSACS: Logic, Model Checking, Formal Specifications
Chair: Joost-Pieter Katoen
Room: Sala Londra
11:10
Béatrice Bérard, Benjamin Monmege, B Srivathsan and Arnab Sur.
11:30
Mathieu Lehaut, Anca Muscholl and Nir Piterman
11:50
Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann and Aniello Murano.
12:10
Bernd Finkbeiner, Hadar Frenkel and Tim Rohde.
FM4All
Chair: Luigia Petre
Room: Sala Berlino
10:30
RUST
Chair:
Room: Sala Parigi
10:30
Soteria Rust: Efficient Symbolic Execution for Rust
Opale Sjöstedt, Sacha-Élie Ayoun and Azalea Raad
11:00
Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust
Florian Sextl
11:30
Scylla: Translating an Applicative Subset of C to Safe Rust
Aymeric Fromherz and Jonathan Protzenko
12:00
RustMC: Automated Verification of Real-World Concurrent Rust
Oliver Pearce, Dan O'Keeffe and Julien Lange
12:30
Lunch Break
Room: Expo Area
14:00
Leonardo de Moura: The Lean Programming Language and Theorem Prover (Invited Tutorial)
Chair: Jan Kofron
Room: Sala 500
15:30
Tool Demos and Posters (with Coffee)
Chairs: Jan Kofron and Laura Kovács
Room: Expo Area
16:00
Coffee Break with Tool Demos and Posters
Chairs: Jan Kofron and Laura Kovács
Room: Expo Area
TACAS: Software Verification
Chair: Arnd Hartmanns
Room: Sala 500
16:30
Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky, Mario Reja and Mikheil Rukhaia.
17:10
Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee and Thomas Lemberger.
17:30
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill and Clark Barrett.
17:50
Guy Amir, Mark Barbone, Nicolas Amat and Jules Jacobs.
18:10
Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi and Nicolas Troquard.
FASE: Advanced SW Development
Chair: Artur Boronat
Room: Sala Madrid
16:30
Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao.
16:50
Mina Yavari and Damian Arellanes.
17:10
Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert.
17:30
Valentim Romão, Rafael Soares, Luis Rodrigues and Vasco Manquinho.
17:50
Muhammad Rizwan Ali, Violet Ka I Pun and Guillermo Román-Díez.
18:10
Youyang Kim, Yaoping Ruan, Young-Kyoon Suh, Liqiang Wang and Byungchul Tak.
FOSSACS: Automata, Games, Concurrency Models
Chair: Lutz Schröder
Room: Sala Londra
16:50
Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul, Sven Schewe, Friedrich Slivovsky, Qiyi Tang, Dominik Wojtczak and Shufang Zhu.
17:10
Isa Vialard, Joël Ouaknine and Quentin Guilmant.
17:30
Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey and Oscar Peyron.
17:50
Hernán Melgratti, Claudio Antares Mezzina and G. Michele Pinna.
18:10
Clotilde Bizière, Jérôme Leroux and Grégoire Sutre.
SV-COMP
Chair: Dirk Beyer and Jan Strejček
Room: Sala Berlino
16:30
Opening and Introduction
Dirk Beyer and Jan Strejček
16:50
C.Huawei-Concurrency-Challenges
Hernán Ponce de León
17:02
Short Tool Presentations
Participants
18:26
Python Subtrack of SV-COMP 2027
Raphaël Monat
RUST
Chair:
Room: Sala Parigi
16:30
Co-development of Code and Proofs for the SymCrypt Cryptographic Library with Aeneas and Lean
Son Ho, Cédric Fournet, Antoine Delignat-Lavaud, Aymeric Fromherz and Jonathan Protzenko
17:00
Place Capability Graphs
Zachary Grannan, Aurea Bílá, Jonáš Fiala, Thomas Mayerl, Peter Müller and Alexander J. Summers
17:30
Prusti Version 2 (and why there is one)
Aurea Bílá, Jonáš Fiala, Grannan Zachary, Thomas Mayerl, Jasper Geer, Peter Müller and Alexander J. Summers
18:00
RUXT: Automatic Compositional Type Safety Refutation
Pedro Carrott, Sacha-Elie Ayoun and Azalea Raad
19:00
ETAPS Reception
Room: Corridoio Nizza
Tuesday 14 April
09:00
Einar Broch Johnsen: Formal Methods meet Digital Twins: Challenges and Opportunities
Chair: Robbert Krebbers
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Probabilistic Model Checking & Software Testing
Chair: Matthias Volk
Room: Sala 500
10:30
Julius Ide, Joost-Pieter Katoen, Hannah Mertens and Tim Quatmann.
11:10
Paolo Baldan, Sebastian Gurke, Barbara König and Florian Wittbold.
11:30
Francesca Randone, Romina Doz, Mirco Tribastone and Luca Bortolussi.
12:10
Charles Moloney, Robert Dyer and Elena Sherman.
ESOP: Concurrency
Chair: Robbert Krebbers
Room: Sala Berlino
10:30
Dylan McDermott and Nobuko Yoshida.
11:10
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper and Yue Yao.
11:30
Duc Than Nguyen and William Mansky.
11:50
Namratha Gangamreddypalli, Constantin Enea and Shaz Qadeer.
12:10
John Derrick, Chelsea Edmonds, Andrei Popescu and Jamie Wright.
FASE: Autonomous Systems/Applications
Chair: Luigia Petre
Room: Sala Parigi
10:30
Andrea Bombarda, Federico Conti, Marcello Minervini, Aurora Francesca Zanenga and Claudio Menghi.
11:10
Annalisa Sergi, Yousef Ahmed Abdel Rahman Shoeib, Andrea Bombarda, Nunzio Marco Bisceglia and Claudio Menghi.
11:30
Mustafa Ghani and Holger Giese.
11:50
Artur Boronat.
FOSSACS: Kleene Algebra, Expressions, String Diagrams, Categorical Logic
Chair: Igor Walukiewicz
Room: Sala Londra
10:30
Liam Chung and Tobias Kappé.
10:50
Yoshiki Nakamura.
11:30
Noé Delorme and Simon Perdrix.
11:50
Thea Li and Vladimir Zamdzhiev.
RUST
Chair:
Room: Sala Madrid
10:30
Verifying the Rust standard library with Creusot
Li-Yao Xia, Arnaud Golfouse and Jacques-Henri Jourdan
11:00
Extending Verus with Logical Atomicity
Aaron Bies
11:30
Supporting Weak Memory in Verus
Natalie Neamtu, Elanor Tang, Laila Elbeheiry, Hoang-Hai Dang, Derek Dreyer, Travis Hance, Chris Hawblitzel and Bryan Parno
12:00
Foundationally Verifying Real-World Rust Programs
Lennard Gäher and Vincent Lafeychine
12:30
Lunch Break
Room: Expo Area
ETAPS Awards and Ask-Me-Anything Session
Room: Sala 500
14:00
Ask-Me-Anything Session
Chair: Sebastian Junges
15:00
ETAPS Awards
Chair: Laura Kovács
RUST
Chair:
Room: Sala Madrid
14:00
Charon: An Analysis Framework for Rust
Guillaume Boisseau, Son Ho and Aymeric Fromherz
14:20
Verifying curve25519-dalek in Verus
Lacramioara Astefanoaei, Sergiu Bursuc, Jure Kukovec, Theodore Ehrenborg, Shaowei Lin and Max Tegmark
14:40
Verifying curve25519-dalek in Lean
Oliver Butterley, Markus Dablander, Alessandro D’Angelo, Hoang Le Truong, Liao Zhang
15:00
HiRustVer: Verifying Industrial Rust Code in Practice – An Ongoing Case Study
Guanyan Li and Haokun Li
15:30
KMIR Meets Real World Rust: An Experience Report
Daniel Cumming
16:00
Coffee Break
Room: Expo Area
TACAS: SAT/SMT I
Chair: Guy Amir
Room: Sala 500
16:30
Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel and Lev Nachmanson.
17:30
João Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait-El-Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Petar Maksimović, Nuno Santos and José Fragoso Santos.
17:50
Ka Lok Wu, Christa Jenkins, Scott Stoller and Omar Chowdhury.
18:10
Chia-Hsuan Lu, Tony Tan and Michael Benedikt.
ESOP: Semantics & Compilation
Chair: Nobuko Yoshida
Room: Sala Berlino
16:50
Guillaume Ambal, Max Stupple, Brijesh Dongol and Azalea Raad.
17:10
Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Taolve Chen, Fu Song and David N. Jansen.
17:30
Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki and Naoki Kobayashi.
17:50
Sidney Congard, Guillaume Munch-Maccagnoni and Rémi Douence.
18:10
Xing Li, Yao Li, Peter Schachte and Christine Rizkallah.
FASE: Testing and Verification
Chair: Dirk Beyer
Room: Sala Parigi
17:10
Dóra Cziborová, Mihály Dobos-Kovács, Kristóf Marussy and András Vörös.
17:30
Dirk Beyer, Thomas Lemberger and Henrik Wachowitz.
FOSSACS: Category Theory, Coalgebra, Metric Systems
Chair: Stefan Milius
Room: Sala Londra
16:50
Paul Wild, Lutz Schröder, Karla Messing, Barbara König and Jonas Forster.
17:10
Quentin Aristote and Daniela Petrisan.
18:10
Matteo Spadetto.
RUST
Chair:
Room: Sala Madrid
16:30
A Program Logic for Tree Borrows
Johannes Hostert and Ralf Jung
17:00
Corten: Foundational Verification for Rust via Separation Logic
Frantisek Farka, Carmine Abate, Sebastian Ertel, Andrei Listochkin and Sven Linker
17:30
RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
Jinhua Wu, Yuting Wang, Liukun Yu and Linglong Meng
Wednesday 15 April
09:00
Monika Henzinger: Guarding Privacy Over Time: Challenges and Solutions in Continuous Data Observation
Chair: Guy Katz
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: Automata
Chair: Roderick Bloem
Room: Sala 500
10:30
Kyveli Doveri, Pierre Ganty and B Srivathsan.
11:10
Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak and Anne-Kathrin Schmuck.
11:30
Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove.
11:50
Jan J.M. Martens and Maurice Laveaux.
12:10
Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya.
ESOP: Verification
Chair: Nils Lommen
Room: Sala Berlino
10:30
Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett and Alex Potanin.
10:50
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Del Valle, Alexandra Silva and Marco Gaboardi.
11:10
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler.
11:30
Philipp Schröer, Darion Haase and Joost-Pieter Katoen.
12:10
Rafael Gonçalves, Frederico Ramos, Pedro Adão and José Fragoso Santos.
FOSSACS: Lambda-Calculus, Program Semantics, Infinite Structures
Chair: Barbara König
Room: Sala Londra
10:30
Adrienne Lancelot, Giulio Manzonetto, Guy McCusker and Gabriele Vanoni.
11:10
Xiaohong Chen, Horatiu Cheval, Dorel Lucanu and Grigore Rosu
11:30
Marco Campion, Isabella Mastroeni, Michele Pasqua and Caterina Urban.
11:50
Annabelle McIver, Natasha Fernandes and Parastoo Sadeghi.
12:10
Aidan Healy and Bartek Klin.
SPIN
Chair: Carlos E. Budde
Room: Sala Parigi
10:30
Invited talk: (Working) Principles and (Open) Challenges in Automated Floating-Point Verification
Eva Darulova
11:30
Control Sensitive Reachability Analysis of Upper-Stack Manipulating Binary Code
Shijie Lin and Tayssir Touilli.
12:00
Visualising CTL witnesses and counterexamples
Arend Rensink (12:00)
Industry Day
Chair: Andrea Basso
Room: Sala Madrid
10:30
SPARK - Latest Industrial Challenges and Feature Development
Invited talk: Claire Dross (AdaCore)
11:10
Formal Methods at OCamlPro: SMT Solving with Alt-Ergo and Symbolic Execution with Owi
Hichem Rami Ait-El-Hara (OCamlPro)
11:30
Towards Sustainable Industrial Use of Formal Verification for Security Certification
Adel Djoudi (Thales) and Nikolai Kosmatov (Thales)
11:50
Semi-Formal Accuracy Analysis of an Industrial Path Computation Algorithm
Franck Vedrine (CEA List), Grégoire Boussu (Thales), Nikolai Kosmatov (Thales) and Bruno Lathuilière (EDF)
12:10
Precomputation: A New Era in Multi-Stage Programming
Seyed Hossein Haeri (Entropy Software Foundation)
12:30
Lunch Break
Room: Expo Area
13:00
ETAPS General Assembly
Chair: Laua Kovács
Room: Sala 500
Industry Day
Chair: Claire Dross
Room: Sala Madrid
14:00
Lean: A Unified Platform for Verification, Programming, and AI
Invited talk: Leonardo de Moura (AWS)
14:40
Check Adherence to Model in Modular and Distributed Cyber-Physical Production Systems
Abdelaziz Ouazzani Chahidi (Agnostic Production Systems), Hasnaa Ait Malek (Agnostic Production Systems), Maxime Morin (Agnostic Production Systems), Nicolas Navarro (Agnostic Production Systems), Darine Rammal (CEA List), Christophe Gaston (CEA List) and Arnault Lapitre (CEA List)
15:00
Semantics-Based Real-Time Verification for Web3
Grigore Rosu (Pi Squared), Dorel Lucanu (Pi Squared) and Xiaohong Chen (Pi Squared)
15:20
Industrial Orchestration of Testing Tools with SeaCoral
Nicolas Berthier (OCamlPro), Steven De Oliveira (OCamlPro), Nikolai Kosmatov (Thales) and Delphine Longuet (Thales)
15:40
On the Lookout for a “Bisimulation” Relation between Trace Sets for Early Design Evaluations
Gurvan Le Guernic (DGA)
Invited Tutorial
Chair: Corina Păsăreanu
Room: Sala 500
15:30
15:30: Tool Demos and Posters (with Coffee Break)
Chairs: Jan Kofron and Laura Kovács
16:00
Coffee Break with Tool Demos and Posters
Chairs: Jan Kofron and Laura Kovács
Room: Expo Area
ESOP: Types
Chair: Stephanie Balzer
Room: Sala Berlino
16:50
Martin Baillon, Assia Mahboubi and Pierre-Marie Pédrot.
17:10
Pedro Ângelo, Atsushi Igarashi, Yuito Murase and Vasco T. Vasconcelos.
17:30
Patrycja Balik, Szymon Jędras and Piotr Polesiuk.
17:50
Hasti Toossi and Ningning Xie.
18:10
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan and Caleb Stanford.
18:20
Mathis Bouverot-Dupuis and Yannick Forster.
TACAS: Static Analysis & Program Verification
Chair: Raz Lotan
Room: Sala 500
16:30
Makoto Hamana and Kento Emoto
16:50
Florian Frohn, Jürgen Giesl, Peter Giesl and Nils Lommen.
17:10
Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler and Kirsten Winter
17:30
Rachel Cleaveland and Clark Barrett.
17:50
Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner.
18:10
Ali Rasim Kocal, Michael Schwarz, Simmo Saan and Helmut Seidl
Industry Day
Chair: Nikolai Kosmatov
Room: Sala Madrid
16:30
From Software Engineering to AI Engineering: Bridging the Research-Industry Gap in the Age of Intelligent Systems
Invited talk: Andrea Basso (Swiss Federal Institute of Technology, EPFL and Stanford University)
17:10
Toward a scalable methodology for Automating Safety Analysis
Stefano Minopoli (Collins Aerospace)
17:30
HPC4AI and Industry: Research Projects and Real-World Applications
Doriana Medic (Univ; of Turin) and Marco Aldinucci (Univ; of Turin)
SPIN
Chair: Matthias Volk
Room: Sala Parigi
16:30
Minimum Reachability Probabilities in Rectangular Automata with Random Clocks
Joanna Delicaris, Erika Abraham and Anne Remke.
17:00
Model Checking of State Based Randomized Systems using Probabilistic Process Algebraic Tools
Shounak Saha and Arpit Sharma. (17:00)
19:00
ETAPS Banquet
Room: Giardino Delle Meraviglie
Thursday 16 April
09:00
Guy Van Den Broeck: Symbolic Reasoning in the Age of Large Language Models
Chair: Sebastian Junges
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: CPS & Quantum
Chair: Kim Larsen
Room: Sala 500
10:30
Lukas König, Christian Schildwächter, Michaela Klauck and Christian Heinzemann.
10:50
Ludovico Battista, Stefano Tonetta and Gianni Zampedri.
11:10
S. Akshay, Prerak Contractor, Paul Gastin, R Govind and B Srivathsan.
11:30
Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan.
11:50
Wei-Jia Huang, Jingyi Mei, Alfons Laarman, Yu-Fang Chen, Christophe Chareton, Kai-Min Chung and Min-Hsiu Hsieh.
12:10
Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou and Jie-Hong Roland Jiang.
ESOP: Analysis
Chair: Guillaume Ambal
Room: Sala Berlino
10:30
Satoshi Kura, Marco Gaboardi, Taro Sekiyama and Hiroshi Unno.
10:50
Han Xu and Di Wang.
11:30
Malo Revel, Thomas Genet and Thomas Jensen.
11:50
Nils Lommen and Jürgen Giesl.
12:10
Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh and Mahesh Viswanathan.
SPIN
Chair: Mattias Ulbrich
Room: Sala Parigi
10:30
Invited talk: Satisfiability-Modulo-Probabilistic Model Checking: Synthesising Robust & Concise Strategies under Uncertainty
Sebastian Junges
11:30
Deductive Verification of Weak Memory Programs with View-based Protocols
Ömer Şakar, Soham Chakraborty, Marieke Huisman and Anton Wijs.
12:00
Crash-free Deductive Verifiers
Wander Nauta, Marcus Gerhold and Marieke Huisman (12:00).
12:30
Lunch Break
Room: Expo Area
TACAS: Model Checking & Hardware Verification
Chair: Rayna Dimitrova
Room: Sala 500
14:00
Roberto Pettinau and Christoph Matheja.
14:20
Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham.
14:40
Frédéric Herbreteau, Gérald Point and Igor Walukiewicz.
15:00
John Nicol and Markus Frohme.
15:20
Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang and Cunxi Yu
15:40
Guangyu Hu, Xiaofeng Zhou, Wei Zhang and Hongce Zhang.
16:00
Valentin Cassano, Pablo Castro, Raul Fervari and Pedro R. D'Argenio.
Diversity, Equity, and Inclusion
Chair: Maurice ter Beek and Ferruccio Damiani
Room: Sala Londra
14:00
Is artificial intelligence neutral? Gen(d)erally no. Reimagining research in STEM through epistemic justice and intersectionality
Viviana Patti
14:30
Detecting a desperate treatment of genders in job interviews with generative AI chatbot (14:30)
Rosa Meo
15:00
AI: Artificially Inaccessible
Dajana Gioffrè and Jacopo Deyla
15:30
Panel Discussion and Q&A (15:30)
Test-Comp
Chair: Dirk Beyer
Room: Sala Madrid
14:00
Opening and Introduction
Dirk Beyer
14:20
Short Tool Presentations
Participants
SPIN
Chair: Vincenzo Ciancia and Arnd Hartmanns
Room: Sala Parigi
14:00
Invited talk: Learning and Proving Array Invariants
Laura Kovács
15:00
Recurrence-seeking Tests for Non-termination
Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, Supratik Chakraborty and Samarjit Chakraborty.
16:00
Coffee Break
Room: Expo Area
TACAS: SAT/SMT II
Chair: Natasha Sharygina
Room: Sala 500
16:30
Tomáš Kolárik, Antti E.J. Hyvärinen, Seyedmasoud Asadzadeh and Natasha Sharygina.
16:50
Dominik Schreiber, Aina Niemetz and Mathias Preiner.
17:10
Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Pascal Fontaine, Cesare Tinelli and Clark Barrett.
17:50
Jakub Horák and Martin Jonáš.
SV-COMP and Test-Comp Community Meeting
Chair: Dirk Beyer and Jan Strejček
Room: Sala Madrid
16:30
Accepted Papers
ESOP
moreless
- Guillaume Ambal, Max Stupple, Brijesh Dongol, Azalea Raad. Specifying and Verifying RDMA Synchronisation
- Pedro Ângelo, Atsushi Igarashi, Yuito Murase, Vasco T. Vasconcelos. Contextual Metaprogramming for Session Types
- Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot. In Cantor Space No One Can Hear You Stream
- Patrycja Balik, Szymon Jędras, Piotr Polesiuk. Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
- Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, Yue Yao. Recursive Logical Relations for Intuitionistic Linear Logic Session Types
- Mathis Bouverot-Dupuis, Yannick Forster. Code Generation via Meta-programming in Dependently Typed Proof Assistants
- Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence. Linear Effects, Exceptions, and Resource Safety
- John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright. Rely-Guarantee Is Coinductive: A Proof-Centered Investigation of Inductively Approximated Coinduction
- Namratha Reddy Gangamreddypalli, Constantin Enea, Shaz Qadeer. Reduction for Structured Concurrent Programs
- Rafael Gonçalves, Frederico Ramos, Pedro Adão, José Fragoso Santos. Specification-Driven Generation of Summaries for Symbolic Execution
- Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
- Ziyue Jin, Di Wang. A Program Logic for Under-approximating Worst-case Resource Usage
- Amir Karniel, Ori Lahav. Causal-Broadcast Memory
- Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno. A Category-Theoretic Framework for Dependent Effect Systems
- Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, Alex Potanin. Validating Quantum State Preparation Programs
- Xing Li, Yao Li, Peter Schachte, Christine Rizkallah. The Memorist Tale: Every Thunk Every Cost All At Once
- Nils Lommen, Jürgen Giesl. Modular Automatic Complexity Analysis of Recursive Integer Programs
- Kazutaka Matsuda, Minh Nguyen, Meng Wang. Lenses for Partially-Specified States
- Dylan McDermott, Nobuko Yoshida. Denotational reasoning for asynchronous multiparty session types
- David Monniaux, Helmut Seidl. Max-Policy Iteration, Revisited
- Duc Than Nguyen, William Mansky. A Formal Interface for Concurrent Search Structure Templates
- Malo Revel, Thomas Genet, Thomas Jensen. Complete Abstractions for Verification of Polymorphic Functions with Equality
- Yasmin Chandini Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh, Mahesh Viswanathan. Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search
- Philipp Schröer, Darion Haase, Joost-Pieter Katoen. Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing
- Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi. Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
- Hasti Toossi, Ningning Xie. Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism
- Toby Ueno, Ankush Das. Practical Refinement Session Type Inference
- Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen, David N. Jansen. A Formally Verified Procedure for Width Inference in FIRRTL
- Han Xu, Di Wang. Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
- Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi. Outrunning Big KATs: Efficient Decision Procedure for Variants of GKAT
- Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford. Auditing Rust Crates Effectively
FASE
moreless
- Mina Yavari and Damian Arellanes. Towards Decentralised Dynamic Reconfiguration of Software Systems
- Andrea Bombarda, Federico Conti, Marcello Minervini, Aurora Francesca Zanenga and Claudio Menghi. Failure Modes and Effects Analysis: An Experience from the E-Bike Domain
- Olivier Zeyen, Karim Tit, Maxime Cordy and Gilles Perrouin. DivKC: A Divide-and-Conquer Approach to Knowledge Compilation
- Giacomo Fantino, Marco Rondina, Antonio Vetro and Juan Carlos De Martin. Quantifying Privacy Risks in Synthetic Data: A Study on Black-Box Membership Inference
- Monika Gupta, Ajay Meena, Anamitra Roy Choudhury, Vijay Arya and Srikanta Bedathur. Revisiting the Role of Natural Language Code Comments in Code Translation
- Kaveh Aryan, Hana Chockler and Mohammad Reza Mousavi. Causal Liability in Autonomous Systems
- Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert. Analyses as First-Class Citizens in Model-Driven Development
- Annalisa Sergi, Yousef Ahmed Abdel Rahman Shoeib, Andrea Bombarda, Nunzio Marco Bisceglia and Claudio Menghi. Search-based Software Testing for Drone Applications: An Experience with the Simulink Environment
- Imane Bousdira, Martin Cooper and Aurélie Hurault. Formally correct search for interpretable DNFs
- Valentim Romão, Rafael Soares, Luis Rodrigues and Vasco Manquinho. Don’t go MAD with Anomalies! Design-time Microservice Anomaly Detection in Migration to Microservices
- Aleksandar S. Dimovski. Abstract Symbolic Finite Automata for Algorithmic Game Semantics
- Erin Woo, Sangyeop Yeo, Hyungkook Jun, Sangcheol Kim, Seung-won Hwang and Yu-Seung Ma. From Words to Code: Do NLP Prompting Strategies Generalize to Code Generation?
- Muhammad Rizwan Ali, Violet Ka I Pun and Guillermo Román-Díez. EasyRPL - A web-based tool for modelling and analysis of cross-organisational workflows
- Bernhard Beckert, Andreas Bremer and Alexander Weigl. Timed Contract Automata
- Dóra Cziborová, Mihály Dobos-Kovács, Kristóf Marussy and András Vörös. Unified Timing-Aware Program Verification
- Youyang Kim, Yaoping Ruan, Young-Kyoon Suh, Liqiang Wang and Byungchul Tak. ForumSeeker: Fusion Retrieval of Online Technical Forums for Effective Troubleshooting
- Yili Jiang, Zhuoran Yan, Ning Ge, Yuan Wang, Jiahao Weng and Chunming Hu. LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability
- Mustafa Ghani and Holger Giese. Modeling and Analyzing Planning-Aware Distributed Cyber-Physical Systems with Timed Graph Transformation Systems
- Dirk Beyer, Thomas Lemberger and Henrik Wachowitz. Testing in Formal Verification via Witness Generation (Empirical Evaluation)
- Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao. QEMI: A Quantum Software Stacks Testing Framework via Equivalence Module Inputs
- Artur Boronat. Composing Clinical Activity Guidance for Multimorbidity via Bounded Relational Analysis
FoSSaCS
moreless
- Paul Wild, Lutz Schröder, Karla Messing, Barbara König and Jonas Forster. Generalized Kantorovich-Rubinstein Duality beyond Hausdorff and Kantorovich
- Liam Chung and Tobias Kappé. Partial Reductions for Kleene Algebra with Single-Word Hypotheses
- Quentin Aristote and Daniela Petrisan. Learning bottom-up tree automata valued in monoidal categories
- Benjamin Plummer and Corina Cirstea. A Coalgebraic Approach to Infinite Games
- Aliaume Lopez, Nathan Lhote and Lia Schuetze. Well-quasi-orderings on word languages
- Jiri Adamek. Quantitative Algebras Presented via Monads
- Jakob Piribauer and Vinzent Zschuppe. The Modal Logic of Abstraction Refinement
- Matteo Spadetto. A 2-categorical approach to the semantics of dependent type theory with computation axioms
- Noé Delorme and Simon Perdrix. Diagrammatic Reasoning with Control as a Constructor, Applications to Quantum Circuits
- Marco Campion, Isabella Mastroeni, Michele Pasqua and Caterina Urban. Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations
- Mariangiola Dezani-Ciancaglini, Besik Dundua and Furio Honsell. Lambda Galore
- Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey and Oscar Peyron. Active Learning Techniques for Pomset Recognizers
- Mayuko Kori and Kazuki Watanabe. A No-go Theorem for Coalgebraic Product Construction
- Aidan Healy and Bartek Klin. Karp’s NP-complete problems over first-order definable structures
- Xiaohong Chen, Horatiu Cheval, Dorel Lucanu and Grigore Rosu. K Definitions as Matching Logic Theories, Formally
- Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann and Aniello Murano. Inquisitive team semantics of LTL
- Annabelle McIver, Natasha Fernandes and Parastoo Sadeghi. Composition Theorems for f-Differential Privacy
- Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul, Sven Schewe, Friedrich Slivovsky, Qiyi Tang, Dominik Wojtczak and Shufang Zhu. The Complexity of Games with Randomised Control
- Robert Hierons and Mohammad Reza Mousavi. Complete FSM Testing Using Strong Separability
- Thea Li and Vladimir Zamdzhiev. Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
- Isa Vialard, Joël Ouaknine and Quentin Guilmant. The Value Problem for Weighted Timed Games with Two Clocks is Undecidable
- Mathieu Lehaut, Anca Muscholl and Nir Piterman. From Trees to Tree-Like: Distribution and Synthesis for Asynchronous Automata
- Yoshiki Nakamura. A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
- Adrienne Lancelot, Giulio Manzonetto, Guy McCusker and Gabriele Vanoni. Interaction Improvement
- Filippo Bonchi and Cipriano Junior Cioffo. Tapes as Stochastic Matrices of String Diagrams
- Hernán Melgratti, Claudio Antares Mezzina and G. Michele Pinna. On Reversibility in Petri Nets
- Yorgo Chamoun and Samuel Mimram. Realization of relational presheaves
- Béatrice Bérard, Benjamin Monmege, B Srivathsan and Arnab Sur. Synthesising Asynchronous Automata from Fair Specifications
- Bernd Finkbeiner, Hadar Frenkel and Tim Rohde. Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
- Clotilde Bizière, Jérôme Leroux and Grégoire Sutre. Bridging the Gap Between Plain VASS and Branching VASS
TACAS
moreless
- Julius Ide, Joost-Pieter Katoen, Hannah Mertens and Tim Quatmann. Multiple Long-Run and omega-Regular Objectives in MDPs
- Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel and Lev Nachmanson. Syntactically Convex Model-Based Projection for Linear Rational Arithmetic
- Angel He and David Parker. Robust Verification of Concurrent Stochastic Games
- Chia-Hsuan Lu, Tony Tan and Michael Benedikt. Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing
- Lukas König, Christian Schildwächter, Michaela Klauck and Christian Heinzemann. Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination
- Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang and Cunxi Yu. ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
- Charles Moloney, Robert Dyer and Elena Sherman. Demonstrating ARG-V’s Generation of Realistic Java Benchmarks for SV-COMP
- Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee and Thomas Lemberger. A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module
- Ali Rasim Kocal, Michael Schwarz, Simmo Saan and Helmut Seidl. Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities
- Ludovico Battista, Stefano Tonetta and Gianni Zampedri. VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems
- Xavier Généreux and Jannis Limperg. Incremental Forward Reasoning for White-Box Proof Search
- Tomáš Kolárik, Antti E.J. Hyvärinen, Seyedmasoud Asadzadeh and Natasha Sharygina. Parallel SMT Solving via Iterative Tree Partitioning
- Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham. Verifying First-Order Temporal Properties of Infinite States Systems via Timers and Rankings
- Valentin Cassano, Pablo Castro, Raul Fervari and Pedro R. D’Argenio. AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic
- Paolo Baldan, Sebastian Gurke, Barbara König and Florian Wittbold. Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
- Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli. Enumerating Choice Terms in Model-Based Quantifier Instantiation
- Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner. Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees
- João Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait-El-Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Petar Maksimović, Nuno Santos and José Fragoso Santos. Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml
- Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin and Georg Zetzsche. Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
- Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan. Quantifier Elimination Meets Treewidth
- Frédéric Herbreteau, Gérald Point and Igor Walukiewicz. Revisiting Stateful Partial-Order Reduction
- Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove. LTLf Learning Meets Boolean Set Cover
- Jan J.M. Martens and Maurice Laveaux. Faster Signature Refinement for Branching Bisimilarity Minimization
- S. Akshay, Prerak Contractor, Paul Gastin, R Govind and B Srivathsan. TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
- Dominik Schreiber, Aina Niemetz and Mathias Preiner. Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
- Kyveli Doveri, Pierre Ganty and B Srivathsan. A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
- Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan. Trace Repair Using Temporal Behavior Trees
- Florian Frohn, Jürgen Giesl, Peter Giesl and Nils Lommen. On Deciding Constant Runtime of Linear Loops
- Rachel Cleaveland and Clark Barrett. Integrating String Reasoning in Symbolic Execution of C Programs
- Ka Lok Wu, Christa Jenkins, Scott Stoller and Omar Chowdhury. Automatically Tightening Access Control Policies with Restricter
- Joshua Clune, Haniel Barbosa and Jeremy Avigad. Hint-Based SMT Proof Reconstruction
- Guy Amir, Mark Barbone, Nicolas Amat and Jules Jacobs. Deciding Serializability in Network Systems
- Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Pascal Fontaine, Cesare Tinelli and Clark Barrett. Exploring the SMT-LIB Benchmark Library
- Wei-Jia Huang, Jingyi Mei, Alfons Laarman, Yu-Fang Chen, Christophe Chareton, Kai-Min Chung and Min-Hsiu Hsieh. Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
- Francesca Randone, Romina Doz, Mirco Tribastone and Luca Bortolussi. DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling
- Yong Lai, Junjie Li and Chuan Luo. SMT(LIA) Sampling with High Diversity
- Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi and Nicolas Troquard. Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring
- Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler and Kirsten Winter. Data Structure Analysis for Binaries
- Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya. MightyPPL : Model Checking MITL with Past and Pnueli Modalities
- Jakub Horák and Martin Jonáš. BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
- Philippe Heim and Rayna Dimitrova. Modular Attractor Acceleration in Infinite-State Games
- Markus Frohme and John Nicol. Deconstructing Subset Construction: Reducing While Determinizing
- Jonáš Fiala and Peter Müller. SMTScope: Automated and Efficient Analysis of SMT Traces
- Roberto Pettinau and Christoph Matheja. CTL-star Model Checking on Infinite Families of Finite-State Labeled Transition Systems
- Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky, Mario Reja and Mikheil Rukhaia. Efficient Verification of Lingua Franca Programs
- Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak and Anne-Kathrin Schmuck. Concurrent Permissive Strategy Templates
- Aina Niemetz and Mathias Preiner. Bit-Precise Interpolation in Bitwuzla
- Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill and Clark Barrett. VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
- Peter Pfeiffer, Mark Peyrer, Daniel Grosse and Martina Seidl. QSOLE: Automatic QBF Equivalence Checking
- Dominik Schreiber, Mathias Fleury, Katalin Fazekas and Armin Biere. Real-time Proof Checking for Distributed Incremental SAT Solving
- Andrea Gilot, Axel Bergström and Eva Darulova. Verifying Floating-Point Programs in Stainless
- Guangyu Hu, Xiaofeng Zhou, Wei Zhang and Hongce Zhang. EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
- Markus Anders, Cayden Codel and Marijn Heule. Orbitopal Fixing in SAT
- Lukas Panneke and Heike Wehrheim. jMT: Testing Correctness of Java Memory Models
- Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou and Jie-Hong Roland Jiang. Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis
- Makoto Hamana and Kento Emoto. ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics