From the 1 of 4 linked papers with an AI index.
4 papers
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.
CobbleDB: Modelling Levelled Storage by Composition
Emilie Ma, Ayush Pandey, Annette Bieniusa +1
We present a composition-based approach to building correctby-construction database backing stores. In previous work, we specified the behaviour of several store variants and prove…
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…
Kintsugi: Decentralized E2EE Key Recovery
Emilie Ma, Martin Kleppmann
Kintsugi is a protocol for key recovery, allowing a user to regain access to end-to-end encrypted data after they have lost their device, but still have their (potentially low-entr…