Program
| Time | Program |
|---|---|
| Sunday | |
| 18:00 – 20:00 | Registration |
| Monday | |
| 08:00 – 09:15 | Registration |
| 09:15 – 09:30 | Opening |
| 09:30 – 11:00 | Session chair: Adnane Saoud 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 | Session chair: Adnane Saoud 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 | Session chair: Zhiming Liu Domain Analysis and Description Dines Bjørner – Technical University of Denmark (DTU) |
| 15:00 – 15:30 | Coffee Break |
| 15:30 – 16:30 | Session chair: Zhiming Liu Domain Analysis and Description Dines Bjørner – Technical University of Denmark (DTU) |
| Tuesday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:30 | Session chair: Sadek Belamfedel Alaoui 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 | Session chair: Sadek Belamfedel Alaoui 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 | Session chair: Mohammed Erradi Verifying Probabilistic Programs: From Theory to Automation Joost-Pieter Katoen – RWTH Aachen University, Germany |
| 15:00 – 15:30 | Coffee Break |
| 15:30 – 16:30 | Session chair: Mohammed Erradi Verifying Probabilistic Programs: From Theory to Automation Joost-Pieter Katoen – RWTH Aachen University, Germany |
| 18:00 – 19:00 | Welcome Reception |
| Wednesday | |
| 08:00 – 09:00 | Registration |
| 08:50 – 09:00 | Opening |
| 09:00 – 10:00 | Session chair: Martin Leucker Fuzz Testing with Temporal Constraints Klaus Havelund – USA |
| 10:00 – 10:30 | Coffee Break |
| 10:30 – 11:00 | Session chair: Heike Wehrheim 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 | Session chair: Heike Wehrheim Timed Monitoring and Monitorability Kim G. Larsen – Aalborg University, Denmark |
| 14:30 – 15:00 | Coffee Break |
| 15:00 – 15:30 | Session chair: Zhiming Liu 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 | Session chair: Zhiming Liu 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 | Session chair: Martin Leucker 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 – 12:10 | Annoucement of ICTAC 2026 |
| 12:10 – 13:30 | Lunch |
| 13:30 – 14:00 | Session chair: Ichiro Hasuo 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 | Session chair: Ahmed Bouajjani 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 Bus departure from ADAM Park Hotel at 18:45 |
| Friday | |
| 08:00 – 09:00 | Registration |
| 09:00 – 10:00 | Session chair: Adnane Saoud 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 | Session chair: Mohammed Erradi 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 | Session chair: Kirstin Peters 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 | Session chair: Abderrahim Ait Wakrime 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 |
| Closing | |
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