25 citations · 45 across the 5 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
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…
cs.LO2023★ 20 cited
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,…