Program
| Time | Program |
|---|---|
| Monday | |
| 08:00 – 09:15 | Registration |
| 09:15 – 09:30 | Opening |
| 09:30 – 11:00 | Tutorial 1: Model Checking, Performance Analysis, Synthesis and Learning for Cyber-Physical Systems Kim G. Larsen – Aalborg University, Denmark |
| 11:00 – 11:30 | Coffee Break |
| 11:30 – 12:30 | Tutorial 1: Model Checking, Performance Analysis, Synthesis and Learning for Cyber-Physical Systems Kim G. Larsen – Aalborg University, Denmark |
| 12:30 – 14:00 | Lunch |
| 14:00 – 15:00 | Tutorial 2: Domain Analysis and Description Dines Bjørner – Technical University of Denmark (DTU) |
| 15:00 – 15:30 | Coffee Break |
| 15:30 – 16:30 | Tutorial 2: Domain Analysis and Description Dines Bjørner – Technical University of Denmark (DTU) |
| Tuesday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:30 | Tutorial 3: Symbolic Control of Nonlinear Systems – Safety, Optimization and Learning Antoine Girard – University Paris-Saclay, CNRS, CentraleSupélec, France |
| 10:30 – 11:00 | Coffee Break |
| 11:00 – 12:00 | Tutorial 3: Symbolic Control of Nonlinear Systems – Safety, Optimization and Learning Antoine Girard – University Paris-Saclay, CNRS, CentraleSupélec, France |
| 12:00 – 13:30 | Lunch |
| 13:30 – 15:00 | Tutorial 4: Verifying Probabilistic Programs: From Theory to Automation Joost-Pieter Katoen – RWTH Aachen University, Germany |
| 15:00 – 15:30 | Coffee Break |
| 15:30 – 16:30 | Tutorial 4: Verifying Probabilistic Programs: From Theory to Automation Joost-Pieter Katoen – RWTH Aachen University, Germany |
| 19:00 – | Welcome Reception |
| Wednesday | |
| 08:00 – 09:00 | Registration |
| 08:50 – 09:00 | Opening |
| 09:00 – 10:00 | Keynote Talk 1: Fuzz Testing with Temporal Constraints Klaus Havelund – NASA’s Jet Propulsion Laboratory, California Institute of Technology, USA |
| 10:00 – 10:30 | Coffee Break |
| 10:30 – 11:00 | From Program Logics towards Language Logics Matteo Cimini |
| 11:00 – 11:30 | A Rely-Guarantee-Based Simulation for Cooperative Semantics Kevin Tran, Johannes Åman Pohjola, Rob Sison, Gerwin Klein |
| 11:30 – 12:00 | Verification of the Release-Acquire Semantics Elli Anastasiadi, Parosh Aziz Abdulla, Mohamed Faouzi Atig, Samuel Grahn |
| 12:00 – 13:30 | Lunch |
| 13:30 – 14:30 | Keynote Talk 2: Timed Monitoring and Monitorability Kim G. Larsen – Aalborg University, Denmark |
| 14:30 – 15:00 | Coffee Break |
| 15:00 – 15:30 | Iteratively Synthesizing ε-Robust Barrier Certificates for Neural Network Controlled Systems Luo Yi, Chen Xin, Dai Jin, Tang Enyi, Li Xuandong |
| 15:30 – 16:00 | AP-Observation Automata for Abstraction-Based Verification of Continuous-Time Systems Sasinee Pruekprasert, Clovis Eberhart |
| 16:00 – 16:30 | Weighted Automata for Exact Inference in Discrete Probabilistic Programs Dominik Geißler, Tobias Winkler |
| Thursday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:00 | Keynote Talk 3: Facing Uncertainty in AI: From Verification To Synthesis Joost-Pieter Katoen – RWTH Aachen University, Germany |
| 10:00 – 10:30 | Coffee Break |
| 10:30 – 11:00 | Active Learning of Symbolic Mealy Automata Kengo Irie, Masaki Waga, Kohei Suenaga |
| 11:00 – 11:30 | Forward and Backward Simulations for Partially Observable Probability Chris Chen, Annabelle McIver, Carroll Morgan |
| 11:30 – 12:00 | The Spiral of Silence in Multi-Agent Models for Opinion Formation David Gaona, Juan Francisco Díaz, Jesús Alexander Aranda, Frank Valencia |
| 12:00 – 13:30 | Lunch |
| 13:30 – 14:00 | Graphical Quadratic Algebra Dario Stein, Fabio Zanasi, Robin Piedeleu, Richard Samuelson |
| 14:00 – 14:30 | Efficient AND Protocols Resistant to Maliciously Revealing a Single Card Koichi Koizumi, Minato Abe, Eikoh Chida, Takaaki Mizuki |
| 14:30 – 15:00 | Coffee Break |
| 15:00 – 15:20 | Explicit Model Checking Engine for Reachability Analysis of Colored Petri Nets (Tool Paper) Emil Normann Brandt, Jens Emil Fink Højriis, Kira Stæhr Pedersen, Jiri Srba |
| 15:20 – 15:40 | PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems Ben Wooding, Viacheslav Horbanov, Abolfazl Lavaei |
| 15:40 – 16:00 | On Computational Aspects of Ordered Matching Problems Jaroslav Nešetřil, Paweł Rzążewski, Andreas Emil Feldmann, Michal Certik |
| 16:00 – 16:20 | Safe Multi-Agent Reinforcement Learning Using Formal Runtime Enforcement: A Case Study Vedanta Mohapatra, Ayush Anand, Srinivas Pinisetty |
| 19:00 – | Conference Banquet |
| Friday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:00 | Keynote Talk 4: Set Invariance for Assume-Guarantee Contracts in System Design Antoine Girard – University Paris-Saclay, CNRS, CentraleSupélec, France |
| 10:00 – 10:30 | Coffee Break |
| 10:30 – 11:00 | On Asynchronous Multiparty Session Types for Federated Learning Ivan Prokic, Simona Prokic, Silvia Ghilezan, Alceste Scalas, Nobuko Yoshida |
| 11:00 – 11:30 | Compositional Interface Refinement Through Subtyping in Probabilistic Session Types Paula Blechschmidt, Kirstin Peters, Uwe Nestmann |
| 11:30 – 12:00 | Efficient Interpolation Beyond Cut-Free Proofs: Admissible Cuts and Optimized Extraction Anela Lolic, Simon Corbard |
| 12:00 – 13:30 | Lunch |
| 13:30 – 14:00 | Multi-Perspective Correctness of Programs Eduard Kamburjan, Dilian Gurov |
| 14:00 – 14:30 | Lean4Less: Eliminating Definitional Equalities from Lean via an Extensional-to-Intensional Translation Rishikesh Vaishnav |
| 14:30 – 15:00 | A Variety of Request-Response Specifications Daichi Aiba, Masaki Waga, Hiroya Fujinami, Koko Muroya, Shuntaro Ouchi, Naoki Ueda, Yosuke Yokoyama, Yuta Wada, Ichiro Hasuo |
| 15:00 – 15:30 | Coffee Break |
| 15:30 – 16:00 | Pomsets for Process Management: A Healthcare Case Study Sourabh Pal, Roberto Guanciale, Ivan Lanese, Emilio Tuosto, Massimo Clo |
| 16:00 – 16:30 | Ulam’s Metric in Higher Dimensions Andrzej Kozik, Sebastian Bala |
Dates
June 14, July 03 July 09, 2025 (AOE)
Abstract submission deadline
June 21 July 09, 2025 (AOE)
Paper submission deadline
August 30, 2025
Accept/Reject notification
September 15 September 20, 2025 (AOE)
Camera-ready submission
November 24-28, 2025
Conference dates
Proceedings
All accepted papers will be published in Springer's LNCS in on-site proceedings "Lecture Notes in Computer Science"