1 citations · 1 across the 2 of their papers we have counts for
3 papers · 1 filter
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory.…
A Verified High-Performance Composable Object Library for Remote Direct Memory Access (Extended Version)
Guillaume Ambal, George Hodgkins, Mark Madler +5
Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU an…
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)
Matt Griffin, Brijesh Dongol, Azalea Raad
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's…