ETAPS 2025 took place in Hamilton, Canada, for the first time out of Europe, and was organized by McMaster University, namely by Claudio Menghi, Mark Lawford, and Melissa Alzaeim. In addition to the work presented at the satellite events during the weekend, 106 papers were accepted and presented at the main conferences ESOP, FASE, FoSSaCS, and TACAS. The second ETAPS Industry Day was organized and attracted a lot of attention. The 31th International SPIN Symposium on Model Checking of Software and the RUST workshop were co-located with ETAPS.
Sessions of the main conferences from Monday to Thursday.
Workshops: LiVe 2025 | RRRR 2025 | TADM 2025 | VerifyThis |
Workshops: ASQAP 2025 | EMW 2025 | FMBC 2025 | PLACES 2025 | TLA | VerifyThis | VSS 2025 |
Ina Schaefer: Correctness-by-Construction—Past, Present and Future (unifying speaker)
FASE: AI and Software Quality
TACAS: Program Analysis
FOSSACS: Games and Logics
RUST WORKSHOP
TACAS: ATP & Rewriting
FOSSACS: Bisimulations
SV-COMP
Diversity & Inclusion
RUST WORKSHOP
TACAS: Model checking
Suguman Bansal (Invited Tutorial)
SV-COMP
RUST WORKSHOP
José Meseguer: Capturing System Designs with Formal Executable Specifications (FASE invited speaker)
TACAS: LTL
ESOP: Types
FASE: MDE
FOSSACS: Semantics
RUST WORKSHOP
TACAS: Verification I
ESOP: Static Analysis
FASE: Fundamentals
RUST WORKSHOP
Ask-me-anything
TACAS: SAT/SMT
Arun Ross (Invited Tutorial)
RUST WORKSHOP
Amal Ahmed: Prose No More: Formally Specifying ABIs using Realistic Realizability (ESOP invited speaker)
TACAS: Proofs and certificates
ESOP: Semantics
FOSSACS: Time and Concurrency
SPIN
INDUSTRY DAY
ETAPS General Assembly
TACAS: Synthesis
ESOP: Concurrency 1
SPIN
INDUSTRY DAY
Tool Demo Session
TACAS: Equivalence checking
ESOP: Fresh Perspectives
FOSSACS: Programs
SPIN
INDUSTRY DAY
Matt Dwyer: Leveraging Abstractions for Validation of Machine Learning Models (unifying speaker)
TACAS: Games
ESOP: Probabilistic Programming
SPIN
TACAS: Verification II
ESOP: Verification
SPIN
Award Winner Presentations
TACAS: Quantum & GPU
ESOP: Concurrency 2
Test-Comp
The Award-Winning Papers, Theses and Tools of ETAPS 2025
EATCS Best Paper Award | Pablo Barenbaum and Eduardo Bonelli: Sharing and Linear Logic with Restricted Access |
EATCS Best Paper Award | Patricia Bouyer, B Srivathsan and Vaishnavi Vishwanath: Model-checking real-time systems: revisiting the alternating automaton route |
EASST Best Paper Award | Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofroň and Natasha Sharygina: Unsatisfiability Proofs for Horn Solving |
EAPLS Best Paper Award | Sung-Shik Jongmans: First-Person Choreographic Programming with Continuation-Passing Communications |
Best Tool Paper Award | Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym and Jan Midtgaard: Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM |
Doctoral Dissertation Award | Kevin Batz: Automated Deductive Verification of Probabilistic Programs |
Test-of-Time Award | K. Rustan M. Leino and Peter Müller: A Basis for Verifying Multi-threaded Programs |
Test-of-Time Tool Award | Daniel Kroening, Peter Schrammel, and Michael Tautschnig: CBMC |
Best Reviewer Award | Peter Müller (ESOP), Naoki Kobayashi (FoSSaCS), Andrian Rutle (FASE), Alan Hu (Tacas) |
Take a look at the photo gallery of ETAPS 2025.
Get back to the ETAPS 2025 homepage to find them!