September 16
| Time | Event | Location |
|---|---|---|
| 09:00-09:20 | Opening | A01 |
| 09:20-10:10 | Session 1 (Chair: Laurentiu Leustean) Tutorial: Mădălina Erașcu Optimization Modulo Theory: A Tutorial Using Z3 and Practical Case Studies (Part 1) | A01 |
| 10:10-10:30 | Coffee Break | |
| 10:30-11:20 | Session 2 (Chair: Mircea Marin) 10:30-10:55: Georgiana Caltais, Mahboobeh Zangiabady, Ervin Zvirbulis – Tracer: A Tool for Race Detection in Software Defined Network Models 10:55-11:20: Georgios V. Pitsiladis, Petros S. Stefaneas – Converting BPMN Diagrams to Privacy Calculus | A01 |
| 11:20-11:40 | Coffee Break | |
| 11:40-13:10 | Session 3 (Chair: Laurentiu Leustean) Tutorial: Mădălina Erașcu Optimization Modulo Theory: A Tutorial Using Z3 and Practical Case Studies (Part 2) | A01 |
| 13:10-14:00 | Lunch | |
| 14:00-15:30 | Session 4 (Chair: Daniel Horpácsi) Tutorial: Vlad Rusu A Hands-on Introduction to the Coq Proof Assistant (Part 1) | A01 |
| 15:30-15:50 | Coffee Break | |
| 15:50-17:20 | Session 5 (Chair: Daniel Horpácsi) Tutorial: Vlad Rusu A Hands-on Introduction to the Coq Proof Assistant (Part 2) | A01 |
| 17:20-18:00 | Session 6 (Chair: Vlad Rusu) 17:20-17:40: Eneia Nicolae Todoran, Gabriel Ciobanu – Abstract Continuation Semantics for Multiparty Interactions in Process Calculi Based on CCS 17:40-18:00: Gabriel Istrate – Towards Geometry-Preserving Reductions Between Constraint Satisfaction Problems | A01 |
September 17
| Time | Event | Location |
|---|---|---|
| 09:00-09:30 | Session 7 (Chair: Mircea Marin) Tutorial: Isabela Drămnesc Introduction to the Theorema System (Part 1) | A01 |
| 09:30-09:50 | Coffee Break | |
| 09:50-11:10 | Session 8 (Chair: Mircea Marin) Tutorial: Isabela Drămnesc Introduction to the Theorema System (Part 2) | A01 |
| 11:10-11:30 | Coffee Break | |
| 11:30-12:50 | Session 9 (Chair: Gabriel Istrate) 11:30-11:50: Lorenzo Capra, Marco Gribaudo – Efficient Performance Analysis of Modular Rewritable Petri Nets 11:50-12:10: Hans Hüttel, Nicky Ask Lund – A Type System for Data Flow and Alias Analysis in ReScript 12:10-12:30: Ștefan Claudiu Susan – Leveraging Slither and Interval Analysis to Build a Static Analysis Tool 12:30-12:50: Vlad Teodorescu, Dorel Lucanu – Static Analysis Framework for Detecting Use-After-Free Bugs in C++ | A01 |
| 13:00-14:00 | Lunch | |
| 14:00-14:50 | Session 10 (Chair: Laura Kovacs) Invited Talk: Nikolaj Bjorner – Formal Methods at Microsoft in the Age of AI | A11 |
| 14:50-15:10 | Coffee Break | |
| 15:10-17:00 | Doctor Honoris Causa Ceremony for Erika Abraham | A11 |
| 17:00-21:00 | Trip to the Aramic Winery and Conference Dinner |
September 18
| Time | Event | Location |
|---|---|---|
| 09:00-09:50 | Session 11 (Chair: Nikolaj Bjorner) Invited Talk: Laura Kovacs – Symbolic Computation in Automated Program Reasoning | A01 |
| 09:50-10:10 | Coffee Break | |
| 10:10-11:10 | Session 12 (Chair: Isabela Drămnesc) 10:10-10:30: Dafina Trufaș – Intuitionistic Propositional Logic in Lean 10:30-10:50: Ádám Kurucz, Péter Bereczky, Dániel Horpácsi – Unification in Matching Logic — Revisited 10:50-11:10: Adriana Balan, Silviu-George Pantelimon – Optics, Functorially: Extended Abstract | A01 |
| 11:10-11:30 | Coffee Break | |
| 11:30-13:00 | Round Table (Chair: Laurentiu Leustean) | |
| 13:00-14:00 | Lunch | |
| 14:00-15:30 | Session 13 (Chair: Mădălina Erașcu) Tutorial: Andrei Voronkov – Induction in Saturation-Based Proving | A11 |
| 15:30-16:00 | Closing | A01 |
