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
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
Room: Sala 500
10:30
Real-time Proof Checking for Distributed Incremental SAT Solving
Dominik Schreiber, Mathias Fleury, Katalin Fazekas and Armin Biere.
10:50
Enumerating Choice Terms in Model-Based Quantifier Instantiation
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli.
11:10
Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa and Jeremy Avigad.
11:30
Incremental Forward Reasoning for White-Box Proof Search
Xavier Généreux and Jannis Limperg.
11:50
QSOLE: Automatic QBF Equivalence Checking
Peter Pfeiffer, Mark Peyrer, Daniel Grosse and Martina Seidl.
12:00
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin and Georg Zetzsche.
12:10
Quantifier Elimination Meets Treewidth
Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan.
FASE: SE and AI
Room: Sala Madrid
10:30
Revisiting the Role of Natural Language Code Comments in Code Translation*
Monika Gupta, Ajay Meena, Anamitra Roy Choudhury, Vijay Arya and Srikanta Bedathur.
10:50
From Words to Code: Do NLP Prompting Strategies Generalize to Code Generation?
Erin Woo, Sangyeop Yeo, Hyungkook Jun, Sangcheol Kim, Seung-won Hwang and Yu-Seung Ma.
11:10
LusGen: Leveraging LLMs for Safety-Critical Lustre Design and Requirements Traceability
Yili Jiang, Zhuoran Yan, Ning Ge, Yuan Wang, Jiahao Weng and Chunming Hu.
11:30
Quantifying Privacy Risks in Synthetic Data: A Study on Black-Box Membership Inference
Giacomo Fantino, Marco Rondina, Antonio Vetro' and Juan Carlos De Martin.
11:50
Formally correct search for interpretable DNFs
Imane Bousdira, Martin Cooper and Aurélie Hurault.
12:10
DivKC: A Divide-and-Conquer Approach to Knowledge Compilation
Olivier Zeyen, Karim Tit, Maxime Cordy and Gilles Perrouin.
FOSSACS: Logic, Model Checking, Formal Specifications
Room: Sala Londra
10:30
The Modal Logic of Abstraction Refinement
Jakob Piribauer and Vinzent Zschuppe.
10:50
Complete FSM Testing Using Strong Separability
Robert Hierons and Mohammad Reza Mousavi.
11:10
Synthesising Asynchronous Automata from Fair Specifications
Béatrice Bérard, Benjamin Monmege, B Srivathsan and Arnab Sur.
11:30
From Trees to Tree-Like: Distribution and Synthesis for Asynchronous Automata
Mathieu Lehaut, Anca Muscholl and Nir Piterman
11:50
Inquisitive team semantics of LTL
Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann and Aniello Murano.
12:10
Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
Bernd Finkbeiner, Hadar Frenkel and Tim Rohde.
RUST
Chair:
Room: Sala Parigi
10:30
12:30
Lunch Break
Room: Expo Area
14:00
Leonardo de Moura: The Lean Programming Language and Theorem Prover (Invited Tutorial)
Chair: Guy Katz
Room: Sala 500
15:30
Tool Demos (with Coffee)
Room: Expo Area
16:00
Coffee Break with Tool Demos
Room: Expo Area
TACAS: Software Verification
Room: Sala 500
16:30
Efficient Verification of Lingua Franca Programs
Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky, Mario Reja and Mikheil Rukhaia.
16:50
Verifying Floating-Point Programs in Stainless
Andrea Gilot, Axel Bergström and Eva Darulova.
17:10
A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module*
Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee and Thomas Lemberger.
17:30
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill and Clark Barrett.
17:50
Deciding Serializability in Network Systems
Guy Amir, Mark Barbone, Nicolas Amat and Jules Jacobs.
18:10
Extending FRET with SLEEC Rules: Formalization, Obligation Inference, and Monitoring
Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi and Nicolas Troquard.
FASE: Advanced SW Development
Room: Sala Madrid
16:30
QEMI: A Quantum Software Stacks Testing Framework via Equivalence Module Inputs
Junjie Luo, Shangzhou Xia, Fuyuan Zhang and Jianjun Zhao.
16:50
Towards Decentralised Dynamic Reconfiguration of Software Systems
Mina Yavari and Damian Arellanes.
17:10
Analyses as First-Class Citizens in Model-Driven Development
Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert.
17:30
Don’t go MAD with Anomalies! Design-time Microservice Anomaly Detection in Migration to Microservices*
Valentim Romão, Rafael Soares, Luis Rodrigues and Vasco Manquinho.
17:50
EasyRPL - A web-based tool for modelling and analysis of cross-organisational workflows
Muhammad Rizwan Ali, Violet Ka I Pun and Guillermo Román-Díez.
18:10
ForumSeeker: Fusion Retrieval of Online Technical Forums for Effective Troubleshooting
Youyang Kim, Yaoping Ruan, Young-Kyoon Suh, Liqiang Wang and Byungchul Tak.
FOSSACS: Automata, Games, Concurrency Models
Room: Sala Londra
16:30
Well-quasi-orderings on word languages
Aliaume Lopez, Nathan Lhote and Lia Schuetze
16:50
The Complexity of Games with Randomised Control
Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul, Sven Schewe, Friedrich Slivovsky, Qiyi Tang, Dominik Wojtczak and Shufang Zhu.
17:10
The Value Problem for Weighted Timed Games with Two Clocks is Undecidable*
Isa Vialard, Joël Ouaknine and Quentin Guilmant.
17:30
Active Learning Techniques for Pomset Recognizers
Adrien Pommellet, Amazigh Amrane, Edgar Delaporte, Geoffroy Du Prey and Oscar Peyron.
17:50
On Reversibility in Petri Nets
Hernán Melgratti, Claudio Antares Mezzina and G. Michele Pinna.
18:10
Bridging the Gap Between Plain VASS and Branching VASS
Clotilde Bizière, Jérôme Leroux and Grégoire Sutre.
SV-Comp
Chair:
Room: Sala Berlino
16:30
RUST
Chair:
Room: Sala Parigi
16:30
19:00
ETAPS Reception
Room: Corridoio Nizza