We transport multi-stage programming from functional to relational programming, with novel constructs to give programmers control over staging and non-determinism. We stage interpreters written as relations, in which the programs under interpretation can contain holes representing unknown expressions or values. By compiling the known parts without interpretive overhead and deferring interpretation to run time only for the unknown parts, we compound the benefits of staging (e.g., turning interpreters into compilers) and relational interpretation (e.g., turning functions into relations and synthesizing from sketches). We extend miniKanren with staging constructs and apply the resulting multi-stage language to relational interpreters for subsets of Racket and miniKanren as well as a relational recognizer for context-free grammars. We demonstrate significant performance gains across multiple synthesis problems, systematically comparing unstaged and staged computation, as well as indicatively comparing with an existing hand-tuned relational interpreter.

An edge 2-coloring is a coloring of the edges of an undirected graph such that each vertex is incident to edges of at most two distinct colors. In the maximum edge 2-coloring problem, the input is an undirected graph, and the goal is to find an edge 2-coloring using the maximum possible number of colors.

The maximum edge 2-coloring problem is known to be APX-hard, and the best known approximation factor is 2. Approximation algorithms with a factor better than 2 are known only for particular classes of graphs that have a perfect matching.

In this talk, we present a 9/5-approximation algorithm for the maximum edge 2-coloring problem on bipartite graphs.

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.