2 citations · 10 across the 14 of their papers we have counts for
15 papers
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…
Soteria: Efficient Symbolic Execution as a Functional Library
Sacha-Élie Ayoun, Opale Sjöstedt, Azalea Raad
Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach…
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…
U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
Flavio Ascari, Roberto Bruni, Roberta Gori +1
O'Hearn's Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms…
Non-Termination Proving: 100 Million LoC and Beyond
Julien Vanegue, Jules Villard, Peter O'Hearn +1
We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximate…
Bayesian Separation Logic
Shing Hin Ho, Nicolas Wu, Azalea Raad
Bayesian probabilistic programming languages (BPPLs) let users denote statistical models as code while the interpreter infers the posterior distribution. The semantics of BPPLs are…
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…
Extending the C/C++ Memory Model with Inline Assembly
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis +1
Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive…
Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour
Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis +2
Memory persistency models provide a foundation for persistent programming by specifying which (and when) writes to non-volatile memory (NVM) become persistent. Memory persistency m…
Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version)
Azalea Raad, Ori Lahav, John Wickerson +2
Software Transactional Memory (STM) is an extensively studied paradigm that provides an easy-to-use mechanism for thread safety and concurrency control. With the recent advent of b…
Specifying and Verifying Persistent Libraries
Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of t…
The Path to Durable Linearizability
Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a po…
View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version)
Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav +2
The rise of persistent memory is disrupting computing to its core. Our work aims to help programmers navigate this brave new world by providing a program logic for reasoning about…
Data Consistency in Transactional Storage Systems: a Centralised Approach
Shale Xiong, Andrea Cerone, Azalea Raad +1
We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on ab…
On the Semantics of Snapshot Isolation
Azalea Raad, Ori Lahav, Viktor Vafeiadis
Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). Its semantics is formally defi…