GLaDOS@Michigan
Graduate Laboratory for Distributed and Operating Systems @ The University of Michigan in Ann Arbor
Pinned Repositories
Aegean
The source code for the implementation and evaluation of the Aegean replication framework
CodeLab-ToyLock
I4
The code base for the I4 prototype, as described in the SOSP '19 paper "I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols"
IronFleet
IronSpec
Kondo
MC-Evals
proof-user-study
Sift
The code base for the Sift prototype, as described in the ATC '22 paper "Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems"
verification-class
Material for the class on verification of distributed and asynchronous systems, developed by Jon Howell and Manos Kapritsos
GLaDOS@Michigan's Repositories
GLaDOS-Michigan/I4
The code base for the I4 prototype, as described in the SOSP '19 paper "I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols"
GLaDOS-Michigan/Aegean
The source code for the implementation and evaluation of the Aegean replication framework
GLaDOS-Michigan/verification-class
Material for the class on verification of distributed and asynchronous systems, developed by Jon Howell and Manos Kapritsos
GLaDOS-Michigan/Kondo
GLaDOS-Michigan/MC-Evals
GLaDOS-Michigan/IronFleet
GLaDOS-Michigan/IronSpec
GLaDOS-Michigan/Sift
The code base for the Sift prototype, as described in the ATC '22 paper "Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems"
GLaDOS-Michigan/CodeLab-ToyLock
GLaDOS-Michigan/proof-user-study
GLaDOS-Michigan/avr
Reads a Verilog file and performs property checking.
GLaDOS-Michigan/dafny-holeEval
GLaDOS-Michigan/dafnyMC
Integrating protocol debugging workflows into dafny
GLaDOS-Michigan/GLaDOS-Michigan.github.io
GLaDOS-Michigan/IronSpec-dafny-grpc-server
GLaDOS-Michigan/ivy
IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
GLaDOS-Michigan/pitometer
Verifying real-time performance guarantees for distributed systems