1 citations · 1 across the 2 of their papers we have counts for
5 papers
FlintKV: A Fast Durable Storage Engine for Modern Databases
Sergey Egorov, Gregory Chockler, Brijesh Dongol +2
Byte-addressable non-volatile memory (NVM) offers an opportunity to rethink storage engine architectures. While recent NVM key-value stores achieve high throughput for ingestion an…
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.…
Specifying and Verifying RDMA Synchronisation (Extended Version)
Guillaume Ambal, Max Stupple, Brijesh Dongol +1
Remote direct memory access (RDMA) allows a machine to directly read from and write to the memory of remote machine, enabling high-throughput, low-latency data transfer. Ensuring c…
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…