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).

Passive testing is an approach to verify system behavior by observing logs from normal operation, without actively injecting test stimuli. This paper presents an industrial case study of applying passive testing in the domain of vehicular embedded systems, utilizing two specialized tools: Timed Easy Approach to Requirements Syntax (T-EARS) for specifying temporal requirements, and Napkin Studio for evaluating these requirements against real system execution logs. We collaborated with Volvo Construction Equipment (VCE) to translate a set of natural language requirements into structured T-EARS specifications. Then we used Napkin Studio to test these requirements against recorded machine log data passively. We evaluate the feasibility of this approach, the extent to which it can detect requirement violations or injected faults, and the perceptions of industry stakeholders regarding the adoption of such passive tests in their verification process. The results show that a majority of functional requirements can be expressed as Guarded Assertions (GAs) and validated on logs, uncovering specific issues. Stakeholders found the method promising for improving test coverage and efficiency, although integration challenges (e.g., log signal inconsistencies and tool usability issues) were noted. Overall, this work provides empirical evidence that passive testing with T-EARS and Napkin Studio can complement traditional hardware-in-the-loop testing, offering a scalable and non-intrusive verification approach in developing vehicular systems.

In this talk I will look at the application of causality to debugging models and explainability. Specifically, I will talk about actual causality as introduced by Halpern and Pearl, and its quantitative extensions. This theory turns out to be extremely useful in various areas of computer science due to a good match between the results it produces and our intuition. It turns out to be particularly useful for explaining the outputs of large AI systems. I will argue that explainability can be viewed as a debugging technique and illustrate this approach with a number of examples. I will discuss the differences between the traditional view of explainability as a human-oriented technique and the type of explainability we are proposing, which is essentially a window inside the (otherwise black-box) system. The talk is reasonably self-contained and does not assume any prior knowledge in AI/ML.