Issue Downloads
Prophecy Made Simple
Prophecy variables were introduced in the article “The Existence of Refinement Mappings” by Abadi and Lamport. They were difficult to use in practice. We describe a new kind of prophecy variable that we find much easier to use. We also reformulate ideas ...
Gradualizing the Calculus of Inductive Constructions
We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial trade-off between graduality and the key properties of normalization and ...
What’s Decidable About Causally Consistent Shared Memory?
While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, the decidability of safety verification for (finite-state) concurrent programs running under causally consistent shared memories is still ...
Solving Program Sketches with Large Integer Values
Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the ...
TF-Coder: Program Synthesis for Tensor Manipulations
The success and popularity of deep learning is on the rise, partially due to powerful deep learning frameworks such as TensorFlow and PyTorch, which make it easier to develop deep learning models. However, these libraries also come with steep learning ...
Fast Graph Simplification for Interleaved-Dyck Reachability
Many program-analysis problems can be formulated as graph-reachability problems. Interleaved Dyck language reachability (InterDyck-reachability) is a fundamental framework to express a wide variety of program-analysis problems over edge-labeled graphs. ...
Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility
- Jacob R. Lorch,
- Yixuan Chen,
- Manos Kapritsos,
- Haojun Ma,
- Bryan Parno,
- Shaz Qadeer,
- Upamanyu Sharma,
- James R. Wilcox,
- Xueyuan Zhao
Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, ...