Theoretical Aspects of Computing - ICTAC 2025
Description
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.
More details
Other editions
Additional editions
Content
.- 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.