AI-based components have become integral to Cyber-Physical Systems (CPS), enabling transformative functionalities across various domains including transportation, energy, and medicine. Specifically, machine learning components are now widely used for perception, control, and decision-making in safety-critical applications, necessitating rigorous verification methods to ensure safe deployment in real-world environments.

In this talk, we present a formal approach for verifying the safety of AI-enabled CPS. We focus on closed-loop systems that integrate dynamical models of physical processes with neural network-based perception and control modules. We explore two verification scenarios: (1) controllers implemented as neural networks, and (2) perception pipelines combining camera models with neural networks. A key challenge in both settings is the scalability of verification algorithms, particularly due to the large size of neural networks and the complexity introduced by image-based perception.

To address these challenges, we propose abstraction techniques that simplify system representations and make verification tractable. Specifically, we introduce two novel data structures: Interval Neural Networks, which provide abstract representations of neural network behaviors, and Interval Images, which serve as abstract symbolic representations of a set of images. We also present novel abstraction-refinement algorithms that efficiently search for small abstractions to prove system safety. Our experimental results demonstrate that these abstraction-refinement algorithms significantly improve scalability and efficiency by quickly identifying small abstractions to prove safety, enabling the analysis of complex, large-scale AI-enabled CPS.

We also discuss verification approaches for evolving neural networks and highlight ongoing work on stability analysis, refinement checking, compositional analysis, and related challenges.

Given k nondeterministic finite automata (NFA), finding an NFA that recognises the intersection of their languages is a basic problem in automata theory. We observe that the classical Cartesian product construction is non-optimal in the worst case, that is, if the automata have many transitions. For a fixed alphabet, the Cartesian product of two NFA may have Θ(m²) transitions if these NFA have at most n states and m transitions each. In this talk, we describe alternative constructions with O(mn) transitions; or O(mn^(k − 1)) for the intersection of k NFA (for fixed k ≥ 2 and alphabet Σ). This gives a faster algorithm for deciding NFA intersection emptiness, that is, deciding whether k given NFA accept a word in common.

We also show that this new algorithm is optimal, unless there exists a breakthrough combinatorial algorithm for detecting (k + 1)-cliques in undirected graphs.

Lastly, we show how these new product constructions allow us to certify NFA intersection emptiness faster.

We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a sound and complete certificate for refuting equivalence and similarity.

Private Set Intersection (PSI) enables two parties to compute the intersection of their datasets without revealing any elements outside the intersection. Many solid protocols exist, but recent attacks have shown that input privacy can sometimes be compromised - even in maliciously secure protocols. These attacks make use of malicious input and our goal today is to protect against this threat.

To mitigate these types of attacks, Authorized PSI (APSI) introduces a trusted third-party judge who authorizes the input prior to the intersection. However, trusting a judge with all your elements may be impractical or undesirable. Building on this idea, Falzon and Markatou (PETS 2025) proposed Partial-APSI, a privacy-preserving variant of APSI where only a portion of each input set is revealed to the judge. Unfortunately, their protocol suffers from substantial bandwidth costs. In this presentation we will construct a bandwidth-efficient Partial-APSI protocol that significantly outperforms Falzon and Markatou’s approach—both in theory and in practice (Euro S&P 2026). And then the final question, can we obtain the same functionality without a judge, maybe with zero-knowledge proofs?

Learning a graph from nodal features is a central problem in network science and statistics, with a history spanning more than 50 years. In recent years, numerous graph-learning algorithms have emerged from the field of graph signal processing (GSP). This talk has three main objectives: (i) to explain different GSP-based graph-learning methods and compare them with classical statistical approaches, (ii) to review recent GSP-based graph-learning results, and (iii) to briefly discuss current trends, challenges, and future directions. While the focus will be on the so-called network association problem (where observations from all nodes are available but no links are known), we will also consider link prediction (where some links are observed) and network tomography (where some nodes remain unobserved, relating to latent-variable graphical lasso).