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
10:00
Coffee Break
TACAS: Proofs and Quantifier Elimination
Room:
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:
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:
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:
10:30
12:30
Lunch Break
15:30
Tool Demos (with Coffee)
16:00
Coffee Break with Tool Demos
TACAS: Software Verification
Room:
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
When One Message Tells the Whole Story: 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:
16:30
Towards Decentralised Dynamic Reconfiguration of Software Systems
Mina Yavari and Damian Arellanes.
16:50
Analyses as First-Class Citizens in Model-Driven Development
Tianhai Liu, Shmuel Tyszberowicz and Bernhard Beckert.
17:10
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:30
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.
17:50
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:
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:
16:30
RUST
Chair:
Room:
16:30
19:00
ETAPS Reception