GitXplorerGitXplorer
m

argosy

public
11 stars
6 forks
0 issues

Commits

List of commits on branch master.
Verified
9fa42b78b7f9b7b989fb3434dfbfec4abcfcbff8

Merge pull request #7 from proux01/stdlib_repo

ttchajed committed 3 days ago
Verified
60bee41110cd2759fbc047b9eada9ed93dc9353f

Update CI action

ttchajed committed 3 days ago
Unverified
2cffe9261180dda86a736689a34f1195b16b4434

Adapt to https://github.com/coq/coq/pull/19530

pproux01 committed 2 months ago
Verified
a6a5aa0d3868efd4ada0b40927b5748e5d8967d3

Merge pull request #6 from ppedrot/hint-locality-error

ttchajed committed 2 years ago
Unverified
c6b407859832b4b7642edafc13585029e5afee29

Adapt w.r.t. coq/coq#16004.

pppedrot committed 2 years ago
Unverified
29c5c17010f93b432539da5e94ced84b46098a4b

Bump submodules.

pppedrot committed 2 years ago

README

The README file for this repository.

Argosy: verifying layered storage systems with recovery refinement

CI

Proving crash safety of systems by proving an implementation refines a specification. Argosy supports implementing layered storage systems with a recovery procedure per layer, and modular verification of each layer independent of the other recovery procedures. Argosy also includes an implementation of Crash Hoare Logic (CHL), a program logic based on Hoare logic for proving an invariant for recovery reasoning.

Using Argosy we verified an extended example consisting of a write-ahead log running on top of a disk replication system. See README.md for details on extracting and running the example.

Compiling

We develop Argosy using Coq master. It should also be compatible with Coq 8.14 and 8.15, which are tested as part of continuous integration.

This project uses git submodules to include several dependencies. Before compiling, run git submodule update --init --recursive to set those up.

To compile just run make with Coq on your $PATH.

Details on extraction for the logging example are in its own README.md.