Grove: a Separation-Logic Library for Verifying Distributed Systems

Grove: a Separation-Logic Library for Verifying Distributed Systems

Bibliographic Details
Main Authors:	Sharma, Upamanyu, Jung, Ralf, Tassarotti, Joseph, Kaashoek, Frans, Zeldovich, Nickolai
Other Authors:	Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
Format:	Article
Language:	English
Published:	ACM\|ACM SIGOPS 29th Symposium on Operating Systems Principles 2023
Online Access:	https://hdl.handle.net/1721.1/152987

Similar Items

Modular Verification of Distributed Systems with Grove
by: Sharma, Upamanyu
Published: (2023)

Verifying concurrent, crash-safe systems with Perennial
by: Chajed, Tej, et al.
Published: (2021)

Argosy: verifying layered storage systems with recovery refinement
by: Chajed, Tej, et al.
Published: (2021)

Extracting and Optimizing Formally Verified Code for Systems Programming
by: Ioannidis, Eleftherios, et al.
Published: (2020)

VerSum: Verifiable Computations over Large Public Logs
by: van den Hooff, Jelle, et al.
Published: (2015)

The K2 Architecture for Trustworthy Hardware Security Modules
by: Athalye, Anish, et al.
Published: (2023)

Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation
by: Athalye, Anish, et al.
Published: (2024)

Verifying a high-performance crash-safe file system using a tree specification
by: Chen, Haogang, et al.
Published: (2021)

Using Crash Hoare logic for certifying the FSCQ file system
by: Chen, Haogang, et al.
Published: (2021)

OpLog: a library for scaling update-heavy data structures
by: Boyd-Wickizer, Silas, et al.
Published: (2014)

Certifying a file system using crash hoare logic
by: Chajed, Tej, et al.
Published: (2019)

A season in the olive grove
by: Arkomanis, Ektoras
Published: (2020)

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
by: Cao, Qinxiang, et al.
Published: (2021)

CPHASH: A cache-partitioned hash table
by: Metreveli, Zviad, et al.
Published: (2012)

Scalable Address Spaces Using Rcu Balanced Trees
by: Clements, Austin T., et al.
Published: (2012)

CPHash: A Cache-Partitioned Hash Table
by: Metreveli, Zviad, et al.
Published: (2011)

RadixVM: Scalable address spaces for multithreaded applications
by: Clements, Austin T., et al.
Published: (2014)

Retroactive auditing
by: Wang, Xi, et al.
Published: (2012)

Hare: a file system for non-cache-coherent multicores
by: Gruenwald, Charles, et al.
Published: (2016)

Towards optimization-safe systems: analyzing the impact of undefined behavior
by: Wang, Xi, et al.
Published: (2014)

A fully verified container library
by: Tschannen, Julian, et al.
Published: (2018)

Scaling a file system to many cores using an operation log
by: Bhat, Srivatsa S., et al.
Published: (2021)

Intrusion Recovery Using Selective Re-execution
by: Kim, Taesoo, et al.
Published: (2011)

Improving application security with data flow assertions
by: Yip, Alexander, et al.
Published: (2011)

Scientific irrigation scheduling for sustainable production in olive groves
by: Aziz, Marjan, et al.
Published: (2022)

A Software Approach to Unifying Multicore Caches
by: Boyd-Wickizer, Silas, et al.
Published: (2011)

Processing Analytical Queries over Encrypted Data
by: Tu, Stephen Lyle, et al.
Published: (2014)

Performal: Formal Verification of Latency Properties for Distributed Systems
by: Zhang, Tony Nuda, et al.
Published: (2023)

Separating Web Applications from User Data Storage with BSTORE
by: Chandra, Ramesh, et al.
Published: (2011)

Specifying crash safety for storage systems
by: Chen, Haogang, et al.
Published: (2021)

Notary: a device for secure transaction approval
by: Athalye, Anish, et al.
Published: (2020)

Logical Disk: A Simple New Approach to Improving File System Performance
by: de Jonge, Wiebren, et al.
Published: (2023)

Software Fault Isolation with Api Integrity and Multi-Principal Modules
by: Mao, Yandong, et al.
Published: (2012)

Linux Kernel Vulnerabilities: State-of-the-Art Defenses and Open Problems
by: Chen, Haogang, et al.
Published: (2012)

Oort: User-Centric Cloud Storage with Global Queries
by: Chajed, Tej, et al.
Published: (2016)

The scalable commutativity rule: designing scalable software for multicore processors
by: Clements, Austin T., et al.
Published: (2014)

The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier
by: Chlipala, Adam
Published: (2014)

Undefined behavior: what happened to my code?
by: Wang, Xi, et al.
Published: (2014)

Concurrency control for multiprocessor event-driven systems
by: Zeldovich, Nickolai, 1981-
Published: (2014)

6.828 Operating System Engineering, Fall 2006
by: Kaashoek, Frans
Published: (2006)