2 citations · 10 across the 14 of their papers we have counts for
6 papers · 1 filter
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…