5 papers
Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification
Finn Hackett, Evan Wrench, Ivan Beschastnikh +1
Linearizability is a standard correctness condition for concurrent objects. It takes a correct by construction sequential specification of a concurrent data structure, and produces…
Specula: Scaling formal specifications for autonomous model checking of system code
Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang +6
Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model chec…
Trace Validation of Unmodified Concurrent Systems with OmniLink
Finn Hackett, Evan Wrench, Peter Macko +3
Concurrent systems are notoriously difficult to validate: subtle bugs may only manifest under rare thread interleavings, and existing tools often require intrusive instrumentation…
SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
Qian Cheng, Ruize Tang, Emilie Ma +7
Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in g…
Understanding Inconsistency in Azure Cosmos DB with TLA+
A. Finn Hackett, Joshua Rowe, Markus Alexander Kuppe
Beyond implementation correctness of a distributed system, it is equally important to understand exactly what users should expect to see from that system. Even if the system itself…