Program
| Time | Programme |
|---|---|
| Monday | |
| 08:00 – 09:15 | Registration |
| 09:15 – 09:30 | Opening |
| 09:30 – 11:00 | Kim G. Larsen Model Checking, Performance Analysis, Synthesis and Learning for Cyber-Physical Systems |
| 11:00 – 11:30 | Break |
| 11:30 – 12:30 | Kim G. Larsen Model Checking, Performance Analysis, Synthesis and Learning for Cyber-Physical Systems |
| 12:30 – 14:00 | Lunch |
| 14:00 – 15:00 | Dines Bjørner Domain Analysis and Description |
| 15:00 – 15:30 | Break |
| 15:30 – 16:30 | Dines Bjørner Domain Analysis and Description |
| Tuesday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:30 | Antoine Girard Symbolic control of nonlinear systems – safety, optimization and learning |
| 10:30 – 11:00 | Break |
| 11:00 – 12:00 | Antoine Girard Symbolic control of nonlinear systems – safety, optimization and learning |
| 12:00 – 13:30 | Lunch |
| 13:30 – 15:00 | Joost-Pieter Katoen Verifying Probabilistic Programs: From Theory to Automation |
| 15:00 – 15:30 | Break |
| 15:30 – 16:30 | Joost-Pieter Katoen Verifying Probabilistic Programs: From Theory to Automation |
| 19:00 – | Welcome Reception |
| Wednesday | |
| 08:00 – 09:00 | Registration |
| 08:50 – 09:00 | Opening |
| 09:00 – 10:00 | Klaus Havelund Fuzz Testing with Temporal Constraints |
| 10:00 – 10:30 | Break |
| 10:30 – 11:00 | Matteo Cimini From Program Logics towards Language Logics |
| 11:00 – 11:30 | Kevin Tran, Johannes Åman Pohjola, Rob Sison, Gerwin Klein A rely-guarantee-based simulation for cooperative semantics |
| 11:30 – 12:00 | Elli Anastasiadi, Parosh Aziz Abdulla, Mohamed Faouzi Atig, Samuel Grahn Verification of the Release-Acquire Semantics |
| 12:00 – 13:30 | Lunch |
| 13:30 – 14:30 | Kim G. Larsen Timed Monitoring and Monitorability |
| 14:30 – 15:00 | Break |
| 15:00 – 15:30 | Luo Yi, Chen Xin, Dai Jin, Tang Enyi, Li Xuandong Iteratively Synthesizing ε-robust Barrier Certificates for Neural Network Controlled Systems |
| 15:30 – 16:00 | Sasinee Pruekprasert, Clovis Eberhart AP-Observation Automata for Abstraction-based Verification of Continuous-time Systems |
| 16:00 – 16:30 | Dominik Geißler, Tobias Winkler Weighted Automata for Exact Inference in Discrete Probabilistic Programs |
| Thursday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:00 | Joost-Pieter Katoen Facing Uncertainty in AI: From Verification To Synthesis |
| 10:00 – 10:30 | Break |
| 10:30 – 11:00 | Kengo Irie, Masaki Waga, Kohei Suenaga Active Learning of Symbolic Mealy Automata |
| 11:00 – 11:30 | Chris Chen, Annabelle McIver, Carroll Morgan Forward and Backward Simulations for Partially Observable Probability |
| 11:30 – 12:00 | David Gaona, Juan Francisco Díaz, Jesús Alexander Aranda, Frank Valencia The Spiral of Silence in Multi-Agent Models for Opinion Formation |
| 12:00 – 13:30 | Lunch |
| 13:30 – 14:00 | Dario Stein, Fabio Zanasi, Robin Piedeleu, Richard Samuelson Graphical Quadratic Algebra |
| 14:00 – 14:30 | Koichi Koizumi, Minato Abe, Eikoh Chida, Takaaki Mizuki |
| 14:30 – 15:00 | Break |
| 15:00 – 15:20 | Emil Normann Brandt, Jens Emil Fink Højriis, Kira Stæhr Pedersen, Jiri Srba Explicit Model Checking Engine for Reachability Analysis of Colored Petri Nets (Tool Paper) |
| 15:20 – 15:40 | Ben Wooding, Viacheslav Horbanov, Abolfazl Lavaei PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems |
| 15:40 – 16:00 | Jaroslav Nešetřil, Paweł Rzążewski, Andreas Emil Feldmann, Michal Certik On Computational Aspects of Ordered Matching Problems |
| 16:00 – 16:20 | Vedanta Mohapatra, Ayush Anand, Srinivas Pinisetty Safe Multi-Agent Reinforcement Learning using Formal Runtime Enforcement: A Case Study |
| 19:00 – | Conference Banquet |
| Friday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:00 | Antoine Girard Set Invariance for Assume-Guarantee Contracts in System Design |
| 10:00 – 10:30 | Break |
| 10:30 – 11:00 | Ivan Prokic, Simona Prokic, Silvia Ghilezan, Alceste Scalas, Nobuko Yoshida On Asynchronous Multiparty Session Types for Federated Learning |
| 11:00 – 11:30 | Paula Blechschmidt, Kirstin Peters, Uwe Nestmann Compositional Interface Refinement Through Subtyping in Probabilistic Session Types |
| 11:30 – 12:00 | Anela Lolic, Simon Corbard Efficient Interpolation Beyond Cut-Free Proofs: Admissible Cuts and Optimized Extraction |
| 12:00 – 13:30 | Lunch |
| 13:30 – 14:00 | Eduard Kamburjan, Dilian Gurov Multi-perspective correctness of programs |
| 14:00 – 14:30 | Rishikesh Vaishnav Lean4Less: Eliminating Definitional Equalities from Lean via an Extensional-to-Intensional Translation |
| 14:30 – 15:00 | Daichi Aiba, Masaki Waga, Hiroya Fujinami, Koko Muroya, Shuntaro Ouchi, Naoki Ueda, Yosuke Yokoyama, Yuta Wada, Ichiro Hasuo A Variety of Request-Response Specifications |
| 15:00 – 15:30 | Break |
| 15:30 – 16:00 | Sourabh Pal, Roberto Guanciale, Ivan Lanese, Emilio Tuosto, Massimo Clo Pomsets for Process Management: a Healthcare Case Study |
| 16:00 – 16:30 | Andrzej Kozik, Sebastian Bala Ulam’s metric in higher dimensions |
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"