Related papers: A First Proof Sprint
The assignment problem is an essential problem in many application fields and frequently used to optimize resource usage. The problem is well understood and various efficient algorithms exist to solve the problem. However, it was unclear…
Adaptive Random Testing (ART) has faced criticism, particularly for its computational inefficiency, as highlighted by Arcuri and Briand. Their analysis clarified how ART requires a quadratic number of distance computations as the number of…
In this document, we prove the convergence of the model proposed in [1], which aims at estimating the LoRaWAN network performance in a single-gateway scenario. First, we provide an analytical proof of the existence of a fixed point solution…
The integration of Formal Verification tools with Large Language Models (LLMs) offers a path to scale software verification beyond manual workflows. However, current methods remain unreliable: without a solid theoretical footing, the…
First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are parametric in the number of nodes in the network or the number…
Several recent papers have introduced a periodic verification mechanism to detect silent errors in iterative solvers. Chen [PPoPP'13, pp. 167--176] has shown how to combine such a verification mechanism (a stability test checking the…
We introduce the first complete formal solution to corrigibility in the off-switch game, with provable guarantees in multi-step, partially observed environments. Our framework consists of five *structurally separate* utility heads --…
Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a…
The alternating current optimal power flow (AC-OPF) problem is critical to power system operations and planning, but it is generally hard to solve due to its nonconvex and large-scale nature. This paper proposes a scalable decomposition…
Multi-Agent Path Finding (MAPF) focuses on determining conflict-free paths for multiple agents navigating through a shared space to reach specified goal locations. This problem becomes computationally challenging, particularly when handling…
The rule $\mathrm{Defeated}(x) \leftarrow \mathrm{Attacks}(y,x),\, \neg \, \mathrm{Defeated}(y)$, evaluated under the well-founded semantics (WFS), yields a unique 3-valued (skeptical) solution of an abstract argumentation framework (AF).…
Multi-agent systems achieve state-of-the-art outcomes through peer collaboration. However, when an agent in the pipeline silently drops a constraint, the system's final output may look correct even though the reasoning chain was quietly…
We study the problem of subspace tracking in the presence of missing data (ST-miss). In recent work, we studied a related problem called robust ST. In this work, we show that a simple modification of our robust ST solution also provably…
Agent frameworks increasingly encode tool-using behavior as explicit workflow graphs, yet safety enforcement remains a runtime concern. These frameworks expose analyzable graph structure through their APIs, enabling pre-deployment static…
The article studies edge coverage for control flow graphs extended with explicit constraints. Achieving a given level of white-box coverage for a given code is a classic problem in software testing. We focus on designing test sets that…
Solving multiagent problems can be an uphill task due to uncertainty in the environment, partial observability, and scalability of the problem at hand. Especially in an urban setting, there are more challenges since we also need to maintain…
The problem of coverage control, i.e., of coordinating multiple agents to optimally cover an area, arises in various applications. However, coverage applications face two major challenges: (1) dealing with nonlinear dynamics while…
A novel model-based approach to verify dynamic networks is proposed; the approach consists in formally describing the network topology and dynamic link parameters. A many sorted first order logic formula is constructed to check the model…
To support operations and passenger-facing services, transit agencies need reliable passenger load trajectories. Currently, load estimates are typically inferred from imperfect sensing systems rather than fully observed, and the accuracy of…
State-of-the-art (SOTA) LLMs have progressed from struggling on proof-based Olympiad problems to solving most of the IMO 2025 problems, with leading systems reportedly handling 5 of 6 problems. Given this progress, we assess how well these…