Log in | Join us

Programme – Satellite Events

Programme of satellite events during the weekend.

ConVeY EMW FMBC MISSION PLACES CMCS VerifyThis WRLA AnalyzeThat COOP LiVe LTT MARS SynCoP TLA+

International Workshop on Continuous Verification of Cyber-Physical Systems (Saturday)

Saturday, April 11, Room: 10
9:00–9:00
Welcome
Alexandra Graß, Max Perschl
9:00–10:00
Keynote: AI-based Control for Underwater Robotics
Erika Ábrahám
10:00–10:30
Coffee Break
10:30–11:00
Multi-Threaded Trace Abstraction
Max Barth
11:00–11:30
When the World Fights Back: Verified Risk-Aware Control Under Adversarial Uncertainty
Deep Ganguly
11:30–12:00
Robustness Certificates for Neural Networks against Adversarial Attacks
Sara Taheri
12:00–12:30
From Neural Networks to Finite-State Automata
Theresa Wasserer
12:30–14:00
Lunch Break
14:00–15:00
Abstract Interpretation
Helmut Seidl
15:00–16:00
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
Marian Lingsch-Rosenfeld
16:00–17:00
Poster Session of recent research
ConVeY PhD Students

ETAPS Mentoring Workshop (Saturday)

Saturday, April 11, Room: 8
8:45–9:00
Welcome & Opening
9:00–10:00
A verification journey: from sequential Java programs to massively-parallel GPU code
Marieke Huisman
10:00–10:30
Coffee break
10:30–11:30
How I Learned to Stop Worrying and Love the Bomb[s]
Emilio Tuosto
11:30–12:30
What I Got Right, What I Got Wrong, and What Happened Anyway: Lessons from My Path
Caterina Urban
12:30–14:00
Lunch Break
14:00–15:00
Connecting the Dots: Navigating Early Academic Life in the Theory and Practice of Software
Claudio Menghi
15:00–16:00
Stressed Out - Personal Reflections on Stress and How to (Possibly) Deal With It
Barbara König
16:00–16:30
Coffee break
16:30–17:30
Conducting Research in the Era of Generative AI and Agentic AI: Rethinking Research Methodology in the Age of Artificial Intelligence
Andrea Basso
17:30–17:40
Closing

7th International Workshop on Formal Methods for Blockchains (Saturday)

Saturday, April 11, Room: 14+13
9:00–9:05
Welcome
Massimo Bartoletti and Diego Marmsoler
9:05–10:05
Scaling Formal Verification Across DeFi Ecosystems
Pamina Georgiou
10:05–10:30
Coffee break
10:30–10:55
Isabelle/EVM: A novel Formalisation of the EVM in Isabelle/HOL
Ashley Card and Diego Marmsoler
10:55–11:20
A Formal Approach to AMM Fee Mechanism with Lean 4
Marco Dessalvi, Massimo Bartoletti and Alberto Lluch-Lafuente
11:20–11:45
Future Monitors in Optimistic Rollups
Margarita Capretto, Martin Ceresa and Cesar Sanchez
11:45–12:10
Deductive Verification of SmartML Smart Contracts with KeY
Tudor Christian Balan, Wolfram Pfeifer and Adele Veschetti
12:10–12:35
Smart Tests for a Smart Contract Language
Miguel Valido and António Ravara
12:35–14:00
Lunch break
14:00–15:00
Verifying zkEVMs: Making Large Scale Formal Verification Work
Alexander Hicks
15:00–15:25
EVM Reentrancy Under the Lens: From Taxonomy to Logic-Rule Detection Pattern
Semia Guesmi, Sabina Rossi, Carla Piazza, Andrea Gasparetto and Matteo Rizzo
15:25–15:45
Towards Property-based Testing of Smart Contracts using Gas Analysis
Elvira Albert, Emanuele De Angelis, Marco Di Ianni, Fabio Fioravanti and Pablo Gordillo
15:45–16:05
Modeling and Verification of Algorand BBA* Consensus
Andrea Esposito, Francesco Pio Rossi, Marco Bernardo and Francesco Fabris
16:00–16:30
Coffee break
16:30–16:50
Exploring the Impact of EIP-8024 opcodes on EVM Bytecode Synthesis
Elvira Albert, Alejandro Hernández-Cerezo and Albert Rubio
16:50–17:10
Act: Specification Language and Verification Framework for Ethereum Smart Contracts
Zoe Paraskevopoulou, Lefteris Lazaropoulos, Anja Petković Komel, Sophie Rain and Alexis Terry
17:10–18:00
Open discussion on smart contract verification benchmark & competition

Models in Space Systems: Integration, Operation, and Networking (Saturday)

Saturday, April 11, Room: 4
8:45–9:00
Welcome & Opening
9:00–10:00
DTN vs non-DTN approaches in Earth to Moon communications
Carlo Caini
10:00–10:30
Coffee Break
10:30–11:00
The Evolution of Uncertainty-Aware DTN Routing: MISSION-Driven Advances
Juan A. Fraire, Pedro D’Argenio, Renato Cherini, Jorge Finochietto, Gregory F. Stock, Holger Hermanns and Arnd Hartmanns
11:00–11:30
Model-Driven Distributed Routing in Satellite Constellations: DisCoRoute and Beyond
Nicolò Benso, Alessandro Compagnoni, Roberto Garello, Gregory F. Stock and Juan A. Fraire
11:30–12:00
Efficient Orbit Information Dissemination for Energy-Constrained Direct-to-Satellite IoT Systems
Santiago M. Henn, Juan A. Fraire, Gregory F. Stock and Holger Hermanns
12:00–12:30
Fault Tree Analysis of Satellite Constellations
Mareike Metzler and Thomas Noll
12:30–14:00
Lunch Break
14:00–14:30
Effective Stochastic Automata Model Checking by Interval Abstraction
Annabell Petri, Arnd Hartmanns and Pedro D'Argenio
14:30–15:00
A Lazy Data Structure to Accelerate a Recent Algorithm for Branching Bisimulation
David N. Jansen and Jan Friso Groote
15:00–15:30
BayesL: a Logical Framework for Bayesian Networks
Stefano M. Nicoletti, Ernst Moritz Hahn and Marielle Stoelinga
15:30–16:00
PICKLES: a Natural Language Framework for Requirement Specification and Model-Based Testing
María Belén Rodríguez and Petra van den Bos
16:00–16:30
Coffee Break
16:30–16:50
DTMC Benchmark Generation
Mark van Wijk
16:50–17:20
Formalising the Cybersecurity Landscape: Tactics and Techniques
Carlos Budde
17:20–18:00
Discussion: The Future Beyond MISSION

Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (Saturday)

Saturday, April 11, Room: 15+12
8:45–9:00
Opening
9:00–10:00
TBA
Franco Barbanera
10:00–10:30
Coffee Break
10:30–10:55
Generating Local Shields for Decentralised Partially Observable Markov Decision Processes
Haoran Yang and Nobuko Yoshida
10:55–11:20
Asynchronous Multiparty Sessions with Mixed Choice
Franco Barbanera and Mariangiola Dezani-Ciancaglini
11:20–11:45
Modelling Distributed Applications with Mixed-Choice Stateful Typestates
Francisco Parrinha, João Mota and António Ravara
11:45–12:10
Branching Out: Existential External Choice in Effpi
Benjamin Robinson and Nobuko Yoshida
12:10–12:30
Probabilistic liveness for multiparty session types
Dylan McDermott
12:30–14:00
Lunch Break
14:00–14:25
Exploiting Aggregate Programming in a Multi-Robot Service Prototype
Gianluca Torta, Giorgio Audrito, Andrea Basso, Daniele Bortoluzzi, Ferruccio Damiani and Giordano Scarso
14:25–14:50
Predicate Subtypes in VerCors
Tycho Dubbeling, Marieke Huisman and Ömer Şakar
14:50–15:15
Towards Multiparty Session Types for Fault-Tolerant Web Applications
Richard Casetta, Nils Gesbert and Pierre Geneves
15:15–15:40
Determinacy with Weak Priorities and Clocks
Luigi Liquori, Michael Mendler and Claude Stolze
15:40–16:00
What’s New in FreeST 5.0: Types, Protocols, and Concurrency
Bernardo Almeida, Pedro Ângelo, Diana Costa, Andreia Mordido, Diogo Poças, Gil Silva and Vasco T. Vasconcelos
16:00–16:30
Coffee Break
16:30–16:50
Borrowing Multiparty Session Types in Rust
Michael Terry and Nobuko Yoshida
16:50–17:10
A Continuation-Based Solution of the Linearity Challenge
Luca Padovani
17:10–17:30
Mechanising Concurrent Quantum Protocols
Angela Bao and Atalay Mert Ileri

18th International Workshop on Coalgebraic Methods in Computer Science (Saturday & Sunday)

Saturday, April 11, Room: theater
9:00–10:00
Invited Talk
Sergey Goncharov
10:00–10:30
Coffee Break
10:30–11:10
Learning Automata with Name Allocation.
Florian Frank, Stefan Milius, Jurriaan Rot and Henning Urbat
11:10–11:50
A Framework for Coalgebraic Reward-Sensitive Bisimulation
Pedro H. Azevedo de Amorim, Mayuko Kori and Koko Muroya
11:50–12:30
The Only Distributive Law Over the Powerset Monad Is the One You Know
Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder and Paul Wild
12:30–14:00
Lunch Break
14:00–15:00
Invited Tutorial
Benjamin Bisping
15:00–15:20
Locally Final Coalgebras in Denotational Semantics
Sergey Goncharov, Marco Peressotti, Stelios Tsampas, Henning Urbat and Stefano Volpe
15:20–15:40
Sheaves on categories of coalgebras
Paul Wang
15:40–16:00
Intrinsically Correct Algorithms and Recursive Coalgebras
Cass Alexandru, Henning Urbat and Thorsten Wißmann
16:00–16:30
Coffee Break
–
Sunday, April 12, Room: theater
9:00–10:00
Keynote Talk
Barbara König
10:00–10:30
Coffee Break
10:30–11:10
Coalgebraic Semantics for Two-agent ATL and its Meta-level Model-checking Complexity
Ryota Kojima and Corina Cirstea
11:10–11:50
Coalgebraic Semantics for Fischer Servi Intuitionistic Modal Logic
Rodrigo Nicolau Almeida, Nick Bezhanishvili and Sarah Dukic
11:50–12:30
Coalgebraic Path Constraints
Todd Schmid
12:30–14:00
Lunch Break
14:00–14:40
On Axioms of Arboreal Categories
Tomáš Jakl and Luca Reggio
14:40–15:00
Break
15:00–15:20
Many-valued Coalgebraic Lindstrom’s Theorem
Chun-Yu Lin
15:20–15:40
Infinite Strategies in Two-Player Games
Benjamin Plummer and Corina Cirstea
15:40–16:00
Computing Distinguishing Formulae for Threshold-Based Behavioural Distances
Jonas Forster, Lutz Schröder, Paul Wild, Barbara König and Pedro Nora
16:00–16:30
Coffee Break

VerifyThis 2026 (Saturday & Sunday)

Saturday, April 11, Room: 2+3
8:45–9:00
Announcements and Introduction
Sacha-Élie Ayoun, Thibault Dardinier
9:00–10:00
Challenge Session 1
10:00–10:30
Coffee Break
10:30–10:45
Teams Introduction
10:45–12:30
Challenge Session 2
12:30–14:00
Lunch Break
14:00–16:00
Challenge Session 3
16:00–16:30
Coffee Break
16:30–17:30
Challenge Session 4
19:30–
Workshop dinner
Sunday, April 12, Room: 2+3
8:45–9:00
9:00–10:00
Invited Tutorial (Part 1) - Velvet: A Multi-Modal Verifier for Effectful Programs
Vladimir Gladshtein, Vitaly Kurin
10:00–10:30
Coffee break
10:30–11:00
Invited Tutorial (Part 2) - Velvet: A Multi-Modal Verifier for Effectful Programs
Vladimir Gladshtein, Vitaly Kurin
11:00–12:30
Judging - Discussion of solutions
12:30–14:00
Lunch
14:00–16:00
Judging - Discussion of solutions
16:00–16:30
Coffee break
16:30–17:30
Judging - Discussion of solutions

The 16th International Workshop on Rewriting Logic and its Applications (Saturday & Sunday)

Saturday, April 11, Room: 5
9:00–10:00
TBA
Carlos Olarte (Invited talk)
10:00–10:30
Coffee Break
10:30–11:00
Generating Invariants by Deductive Model Checking
Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer and Julia Sapiña
11:00–11:30
A Semantic Framework for Symbolic Execution in Maude
Rafael Morales-Palacios, Rubén Rubio and Ignacio Fábregas
11:30–12:00
Bounded Structural Model Finding with Symbolic Data Constraints
Artur Boronat
12:00–12:30
A Maude Framework for Efficient Analysis of Multiformalism Models
Lorenzo Capra
12:30–14:00
Lunch Break
14:00–16:00
Statistical Model Checking with QMaude
Rubén Rubio (Tutorial)
16:00–16:30
Coffee Break
16:30–17:00
The Timed P Transformation for Distributed Real-Time Systems
José Meseguer and Peter Csaba Ölveczky
17:00–17:30
On the translation of Maude programs to modern imperative languages
Rubén Rubio, Beatriz Alcaide García and Adrian Riesco
Sunday, April 12, Room: 5
9:00–10:00
TBA
Canh Minh Do (Invited talk)
10:00–10:30
Coffee Break
10:30–11:00
A Theory of Composable Lingos for Protocol
Víctor García, Santiago Escobar, Catherine Meadows and José Meseguer
11:00–11:30
Space-time deterministic graph rewriting
Pablo Arrighi, Marin Costes, Gilles Dowek and Luidnel Maignan
11:30–12:00
An Algebraic Specification for Quantum Computation in Maude
Canh Minh Do and Kazuhiro Ogata
12:00–12:30
On Generalization of Church-Rosser Strategies for Confluent Abstract Rewriting Systems of the Smallest Uncountable Cardinality
Ievgen Ivanov
12:30–14:00
Lunch Break
14:00–16:00
Confluence of Equational Generalized Term Rewriting Systems with Application to Rewrite Theories and Maude
Salvador Lucas (Tutorial)
16:00–16:30
Coffee Break
16:30–17:00
Equational and Inductive Reasoning for Maude in Athena
Mateo Sanabria, Carlos Varela, Camilo Rocha and Nicolás Cardozo
17:00–17:30
Closing
Camilo Rocha

AnalyzeThat 2026 (Sunday)

Sunday, April 12, Room: 8
8:55–
Welcome from the organizers
Raphaël Monat, Helmut Seidl, Vesal Vojdani
9:00–
Sound Static Analysis at Scale: Practical Lessons from Industry
Jörg Herter
10:00–
Coffee break
10:30–
Presentation of AnalyzeThat by organizers
Raphaël Monat, Helmut Seidl, Vesal Vojdani
10:40–
Broom
Tomáš Dacík, Florian Sextl, Tomáš Vojnar, Adam Rogalewicz, Veronika Šoková, and Florian Zuleger.
11:10–
Codex
Matthieu Lemerre, Mihaela Sighireanu
11:40–
Frama-C
André Maroneze
12:30–
Lunch Break
14:00–
Goblint
Simmo Saan, Jevgenij Protopopov, Ali Rasim Kocal, Michael Schwarz, and Karoliine Holter
14:30–
Mopsa
Raphaël Monat, Antoine Miné
15:00–
Open discussion about identified challenges and future perspectives
16:00–
Coffee break
16:30–
Open discussion, if needed
19:30–
Workshop dinner

7th Workshop on Cooperative Software Verification (Sunday)

Sunday, April 12, Room: 4
9:00–10:00
Cooperative AI-Assisted Formal Verification: Integrating LLMs with Model Checking for Scalable Software Assurance (Keynote)
Lucas C. Cordeiro
10:00–10:30
Coffee Break
10:30–11:00
From Programs to Circuits: Bridging Software and Hardware Model Checking with CPV
Po-Chun Chien
11:00–11:30
A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures
Wolfram Pfeifer, Werner Dietl, Mattias Ulbrich
11:30–12:00
Non-termination Witnesses and Their Validation
Zsófia Ádám, Paulína Ayaziová, Levante Bajczi, Dirk Beyer, Marek Jankola, Marian Lingsch-Rosenfeld, Jan Strejček
12:00–12:30
Transition Invariants Revisited: Termination Witnesses and Their Validation
Marek Jankola
12:30–14:00
Lunch Break
14:00–14:30
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
Marian Lingsch-Rosenfeld
14:30–15:00
Towards Universal Adapters for Verification Tools via LLMs
Cedric Richter
15:00–15:30
Certificates: Bridging the Semantic Gap between Algorithmic and Deductive Verifiers
Matthias Heizmann, Dominik Klumpp, Marian Lingsch-Rosenfeld, Fran Schüssele
15:30–16:00
Precision Reuse for Exchange between Verifiers
Mark Somorjai
16:00–16:30
Coffee Break
16:30–17:00
Kukicha: Augmenting Refinement Type Checking with Deductive Verification
Florian Lanzinger, Mattias Ulbrich, Werner Dietl
17:00–17:30
Rethinking the Witness Standard: Software Witness Guide 2.1
Zsófia Ádám, Paulína Ayaziová, Dirk Beyer, Marian Lingsch-Rosenfeld, Jan Strejček
17:30–18:00
Discussion

10th Workshop on Learning in Verification (Sunday)

Sunday, April 12, Room: 15+12
11:30–12:30
Panel on the new roles of specifications, models and formal synthesis in the AI age
Panelists: Bernhard Beckert, Martin Leucker, Luca Bortolussi, moderated by Jan Kretinsky

Workshop on Logics and Type Theory (Sunday)

Sunday, April 12, Room: 14
8:45–9:00
Opening
9:00–9:30
Stefano's achievements in logic and type theory
Ugo de'Liguoro
9:30–10:00
Ultimate Glivenko?
Peter Schuster
10:00–10:30
Coffee Break
10:30–10:55
Principal Typing for Intersection Types, Forty-Five Years Later
Daniele Pautasso and Simona Ronchi Della Rocca
10:55–11:20
Reversible Computation with Stacks and ''Reversible Management of Failures''
Matteo Palazzo and Luca Roversi
11:20–11:45
Lambdas at the Far Edge: a Tale of Flying Lambdas and Lambdas on Wheels
Giorgio Audrito, Daniele Bortoluzzi, Ferruccio Damiani, Giordano Scarso, Gianluca Torta, Andrea Basso, Monica Cochi, Lorenzo Gusman, Lorenzo Comba, Paolo Gay, Paola Dal Zovo, Giada Galati, Francesco Gallo, Aljaž Grdadolnik, Massimo Pescarollo and Paola Pisano
11:45–12:10
A Core Calculus for Type-safe Product Lines of C Programs
Ferruccio Damiani, Daisuke Kimura, Luca Paolini and Makoto Tatsuta
12:10–12:35
Learning Foundations Beneath the Stars
Felice Cardone and Luca Paolini
12:35–14:00
Lunch Break
14:00–14:30
Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice
Zena M. Ariola, Paul Downen and Hugo Herbelin
14:30–15:00
On the Computational Content of Moduli of Regularity and their Logical Strength
Ulrich Kohlenbach
15:30–16:00
An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus
Rob Nederpelt and Ferruccio Guidi
16:00–16:30
Coffee Break
16:30–17:00
A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
Marc Bezem, Thierry Coquand, Peter Dybjer and Martín Escardó
17:00–17:25
Sensible Intersection Type Theories
Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini and Furio Honsell
17:25–18:00
Stefano's speech, video greetings, presentation of the Festschrift and closing remarks.

7th Workshop on Models for Formal Analysis of Real Systems (Sunday)

Sunday, April 12, Room: 13
10:00–10:30
Coffee Break
10:30–11:30
Keynote 1: Verification meets causality
Christel Baier
11:30–12:30
Session 1: Modelling and Analysis of Economic and Supply Chain Systems
11:30–12:00
Statistical model checking of the Island Model: an established economic agent-based model of endogenous growth
Stefano Blando, Giorgio Fagiolo, Daniele Giachini, Andrea Vandin, and Ernest Ivanaj
12:00–12:30
Modelling and Analysis of Supply Chains using Product Time Petri Nets
Eric Lubat, Pierre-Emmanuel Hladik, Yoann Mateu, and Rémi Sauvere
12:30–14:00
Lunch Break
14:00–15:00
Keynote 2: Analysing Real (Time) Systems with Uppaal, Spreadsheets, and Lince
José Proença
15:00–16:00
Session 2: Modelling and Analysis Tools: Lessons from Case Studies
15:00–15:30
Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
Hubert Garavel
15:30–16:00
Safe and Near-Optimal Gate Control: A Case Study from the Danish West Coast
Martin Kristjansen, Kim Guldstrand Larsen, Marius Mikucionis, and Christian Schilling
16:00–16:30
Coffee Break
19:30–
Workshop dinner

11th International Workshop on Synthesis of Complex Parameters (Sunday)

Sunday, April 12, Room: 1
9:00–10:00
Reduction theorems for effective parameterized verification of round-based distributed algorithms
Nathalie Bertrand
10:00–10:30
Coffee Break
10:30–11:00
S-IMITATOR: Strategy Synthesis for STCTL
Adrien Lacroix
11:00–12:00
How Satisfiability-Modulo-Probabilistic-Model-Checking Finds Robust and Concise Policies
Sebastian Junges
12:00–14:00
Lunch Break
14:00–14:30
The Complexity of Games with Randomised Control
Sarvin Bahmani
14:30–15:30
Synthesizing Temporal Logic Specifications via Learning from Examples
Rajarshi Roy
15:30–16:00
Coffee Break
16:00–17:00
Probabilistic Timed Automata with Clock-Dependent Probabilities
Jeremy Sproston

TLA+ Community Meeting (Sunday)

Sunday, April 12, Room: 10
9:00–9:30
A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments
Q. Delamea, J. Burman, J. Gurhem, S. Vialle
9:30–10:00
A generic hardware in-order pipeline architecture model to capture key temporal properties
J.-P. Bodeveix, A. Bonenfant, T. Carle, M. Filali, C. Rochange, L. Sylvestre
10:00–10:30
Coffee Break
10:30–11:00
Extensible Proof Decomposition Rules for TLAPS
K. Petrauskas
11:00–11:30
Systematic API Testing through Model Checking and Executable Contracts
A.C. Ribeiro, M. Mamede, C. Ferreira
11:30–12:00
Model-based Testing of Practical Distributed Systems in Actor Model
I. Kokorin, E. Chernatskiy, V. Aksenov
12:00–12:30
Interactive symbolic testing with TLA+, Apalache, and LLMs
I. Konnov
12:30–14:00
Lunch Break
14:00–14:50
Thinking in TLA+ – Modeling Judgment for System Design
M. Demirbas
14:50–15:20
P2P2P (PlusCal to PlantUML to PDF)
J. Belzer, J.J. Serrano Mora, A.B. Marcos, C. Lamb
15:20–15:50
Towards Language Model Guided TLA+ Proof Automation
Y. Zhou, S. Tripakis
16:00–16:30
Coffee Break
16:30–17:00
Verifying differential privacy in TLA+ via self-products
U. Yavuz
17:00–17:30
Veil: Multi-Modal Verification of Transition Systems
G. Pîrlea
17:30–18:00
Discussion and closing
19:30–
Workshop Dinner
Main 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