Read more
This book constitutes the proceedings of 22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025, which took place in Marrakesh, Morocco, during November 24 28, 2025.
The 21 full papers, 2 short papers and 1 tool paper presented in this book were carefully reviewed and selected from 64 submissions. The papers were categorized into the following topical sections: Invited Papers; Tutorial; Verification and Synthesis; Session Types; Logic and Theorem Provers; Probabilistic Systems; Automata; Cryptography and Choreography; Algorithms and Complexity; and Tool and Short Papers.
List of contents
.- Invited Papers
.- Fuzz Testing with Temporal Constraints.
.- Facing Uncertainty in AI: From Verification To Synthesis.
.- Timed Monitoring and Monitorability
.- Set Invariance for Assume-Guarantee Contracts in Cyber-Physical Systems Design.
.- Tutorial
.- Domain Analysis & Description.
.- Verification and Synthesis
.- Multi-perspective correctness of programs.
.- A rely-guarantee-based simulation for cooperative semantics.
.- Verification of the Release-Acquire Semantics.
.- Iteratively Synthesizing -robust Barrier Certificates for Neural Network Controlled Systems.
.- Session Types
.- Compositional Interface Refinement Through Subtyping in Probabilistic Session Types.
.- On Asynchronous Multiparty Session Types for Federated Learning.
.- Logic and Theorem Provers
.- Efficient Interpolation Beyond Cut-Free Proofs: Admissible Cuts and Optimized Extraction.
.- Lean4Less: Eliminating Definitional Equalities from Lean via an Extensional-to-Intensional Translation.
.- From Program Logics towards Language Logics.
.- A Variety of Request-Response Specifications.
.- Probabilistic Systems
.- Weighted Automata for Exact Inference in Discrete Probabilistic Programs.
.- Forward and Backward Simulations for Partially Observable Probability.
.- Graphical Quadratic Algebra.
.- Automata
.- Active Learning of Symbolic Mealy Automata.
.- AP-Observation Automata for Abstraction-based Verification of Continuous-time Systems.
.- Cryptography and Choreography
.- Efficient AND Protocols Resistant to Maliciously Revealing a Single Card.
.- Pomsets for Process Management: a Healthcare Case Study.
.- Algorithms and Complexity
.- Ulam s metric in higher dimensions.
.- The Spiral of Silence in Multi-Agent Models for Opinion Formation.
.- Tool and Short Papers
.- Explicit Model Checking Engine for Reachability Analysis of Colored Petri Nets (Tool Paper).
.- PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems.
.- On Computational Aspects of Ordered Matching Problems.
.- Safe Multi-Agent Reinforcement Learning using Formal Runtime Enforcement: A Case Study.
Summary
This book constitutes the proceedings of 22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025, which took place in Marrakesh, Morocco, during November 24–28, 2025.
The 21 full papers, 2 short papers and 1 tool paper presented in this book were carefully reviewed and selected from 64 submissions. The papers were categorized into the following topical sections: Invited Papers; Tutorial; Verification and Synthesis; Session Types; Logic and Theorem Provers; Probabilistic Systems; Automata; Cryptography and Choreography; Algorithms and Complexity; and Tool and Short Papers.
