47 citations · 56 across the 7 of their papers we have counts for
7 papers
A Formal Semantics of C with OpenMP Parallelism (Extended Version)
Ke Du, Anshu Sharma, Liyi Li +1
OpenMP is a popular parallelization framework that lets users transform sequential code into parallel code with a few simple annotations. Unfortunately, it is also easy to inadvert…
Recursive Mutexes in Separation Logic
Ke Du, William Mansky, Paolo G. Giarrusso +1
Mutexes (i.e., locks) are well understood in separation logic, and can be specified in terms of either protecting an invariant or atomically changing the state of the lock. In this…
Proving Logical Atomicity using Lock Invariants
Roshan Sharma, Shengyi Wang, Alexander Oey +3
Logical atomicity has been widely accepted as a specification format for data structures in concurrent separation logic. While both lock-free and lock-based data structures have be…
Bringing Iris into the Verified Software Toolchain
William Mansky
The Verified Software Toolchain (VST) is a system for proving correctness of C programs using separation logic. By connecting to the verified compiler CompCert, it produces the str…
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li +6
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie toge…
Structural Operational Semantics for Control Flow Graph Machines
Dmitri Garbuzov, William Mansky, Christine Rizkallah +1
Compilers use control flow graph (CFG) representations of low-level programs because they are suited to program analysis and optimizations. However, formalizing the behavior and me…
Specifying and Executing Optimizations for Parallel Programs
William Mansky, Dennis Griffith, Elsa L. Gunter
Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers. However, even production compilers have bugs, and these bugs are d…