25 citations · 45 across the 5 of their papers we have counts for
5 papers
Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents
M. Frans Kaashoek, Nickolai Zeldovich
MachCSL is a framework for verifying system software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea beh…
Shipwright: Proving liveness of distributed systems with Byzantine participants
Derek Leung, Nickolai Zeldovich, Frans Kaashoek
Ensuring liveness in a decentralized system, such as PBFT, is critical, because there may not be any single administrator that can restart the system if it encounters a liveness bu…
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti +2
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration,…
A Revised and Verified Proof of the Scalable Commutativity Rule
Lillian Tsai, Eddie Kohler, M. Frans Kaashoek +1
This paper explains a flaw in the published proof of the Scalable Commutativity Rule (SCR), presents a revised and formally verified proof of the SCR in the Coq proof assistant, an…
Report on the NSF Workshop on Formal Methods for Security
Stephen Chong, Joshua Guttman, Anupam Datta +5
Report on the NSF Workshop on Formal Methods for Security, held 19-20 November 2015.