6 papers
Reasoning About Vectors using an SMT Theory of Sequences
Ying Sheng, Andres Nötzli, Andrew Reynolds +7
Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such progra…
The Move Borrow Checker
Sam Blackshear, John Mitchell, Todd Nowacki +1
The Move language provides abstractions for programming with digital assets via a mix of value semantics and reference semantics. Ensuring memory safety in programs with references…
Resources: A Safe Language Abstraction for Money
Sam Blackshear, David L. Dill, Shaz Qadeer +4
Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract pr…
Building Reliable Cloud Services Using P# (Experience Report)
Pantazis Deligiannis, Narayanan Ganapathy, Akash Lal +1
Cloud services must typically be distributed across a large number of machines in order to make use of multiple compute and storage resources. This opens the programmer to several…
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Ahmed Bouajjani, Constantin Enea, Kailiang Ji +1
We address the problem of verifying message passing programs, defined as a set of parallel processes communicating through unbounded FIFO buffers. We introduce a bounded analysis t…
Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking
Shaz Qadeer
The memory model of a shared-memory multiprocessor is a contract between the designer and programmer of the multiprocessor. The sequential consistency memory model specifies a tota…