1 citations · 2 across the 6 of their papers we have counts for
4 papers · 2 filters
TypeDis: A Type System for Disentanglement
Alexandre Moine, Stephanie Balzer, Alex Xu +1
Disentanglement is a runtime property of parallel programs guaranteeing that parallel tasks remain oblivious to each other's allocations. As demonstrated in the MaPLe compiler and…
Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
Tesla Zhang, Asher Kornfeld, Rui Li +3
Semantic typing has become a powerful tool for program verification, applying the technique of logical relations as not only a proof method, but also a device for prescribing progr…
Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
Zachary Kent, Ugur Y. Yavuz, Siddhartha Jayanti +2
In the past decade, many techniques have been developed to prove linearizability, the gold standard of correctness for concurrent data structures. Intuitively, linearizability requ…
A Language-Agnostic Logical Relation for Message-Passing Protocols
Tesla Zhang, Sonya Simkin, Rui Li +2
Today's computing landscape has been gradually shifting to applications targeting distributed and *heterogeneous* systems, such as cloud computing and Internet of Things (IoT) appl…