SYNT 2026

Title: Coverage Games

Abstract. We introduce and study coverage games -- a novel framework for multi-agent planning in settings in which a system operates several agents but does not have full control on them, or interacts with an environment that consists of several agents. The game is played between Coverer and Disruptor. Coverer has a set of objectives and she operates several agents, which interact with Disruptor. Coverer wins if every objective is satisfied by at least one agent. Otherwise, Disruptor wins. Coverage games thus extend traditional two-player games with multiple objectives by allowing a (possibly dynamic) decomposition of the objectives among different agents. Coverage games have many applications, both in settings where the system is Coverer (e.g., multi-robot surveillance, coverage in multi-threaded systems) and settings where it is Disruptor (e.g., prevention of resource exhaustion, ensuring non-congestion). We study the theoretical properties of coverage games, including determinacy, and the ability to a priori decompose the objectives among the agents. We solve the problems of deciding whether Coverer or Disruptor wins, analyze their tight complexity, and consider useful special cases. Joint work with Noam Shenwald

Title: What NP Oracles Can and Cannot Do for Functional Synthesis

Abstract. Functional synthesis tools have scaled dramatically over the past decade, routinely handling specifications with tens of thousands of variables, largely by reducing to sequences of SAT calls and exploiting decades of progress in SAT solving. Despite this practical success, little is known about the theoretical limitations and power of NP-oracle-based approaches to functional synthesis. In this talk, I will discuss our work initiating a systematic investigation into this question. I will first show that naive bit-by-bit learning fails even when small Skolem functions exist, owing to the relational nature of specifications, and that resolution-based interpolation must produce exponential-size circuits under the same conditions, before turning to our main result: an algorithm that uses NP oracles to synthesize small Skolem functions in time polynomial in the size of the specification and the size of the smallest sufficient set of witnesses. Building on this, I will show that a popular interpolation-based preprocessing technique — which applies only when the specification uniquely determines its outputs---is in fact without loss of generality: a randomized polynomial-time reduction shows that general Skolem synthesis reduces to this uniquely-determined case. Joint work with Brendan Juba.

Title: Certificates in AI: Learn but Verify

Abstract. Due to the mind-boggling progress in AI, formal methods may finally get to play a central role in computing. First, because AI-generated code needs checks even more than software written by humans. But more importantly, second, because modern AI can provide or at least support such checks at unprecedented scale. Independently verifiable records of such checks are called certificates. Certificates can take the form of formal proofs, or of critical parts from which such proofs can be reconstructed. For example, in control systems, invariants and barrier functions are certificates for safety; Lyapunov functions and supermartingales, certificates for progress. In synthesis, not only controllers but also certificates can be learned or otherwise AI-generated, often together, and sometimes even represented as neural networks ("neural certificates"). We advocate a synthesis methodology where AI ("learning") is used as much as possible, and logic ("verifying") as little as necessary. This talk is based on joint work and discussions with many collaborators, including Clark Barrett, Krishnendu Chatterjee, Mirco Giacobbe, Mathias Lechner, Kaushik Mallik, Sanjit Seshia, Abhinav Verma, Emily Yu, and Djordje Zikelic.