papers
Publications (3)
cs.SE2026
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…
cs.AI2026
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…
cs.SE2026
Specula: Scaling formal specifications for autonomous model checking of system code
Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang +6
Specula is an autonomous system that uses large language model agents to generate TLA+ specifications for complex system code and then applies model checking to discover bugs.
#formal specifications#model checking#large language models#system code