A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm

You can build this theory using Isabelle2020 and the following command:

isabelle build -D .

Name		Name	Last commit message	Last commit date
Latest commit History 8 Commits
document		document
.gitignore		.gitignore
Co_Snapshot.thy		Co_Snapshot.thy
Distributed_System.thy		Distributed_System.thy
Example.thy		Example.thy
LICENSE		LICENSE
README.md		README.md
ROOT		ROOT
Snapshot.thy		Snapshot.thy
Swap.thy		Swap.thy
Trace.thy		Trace.thy
Util.thy		Util.thy
prepare-for-afp.sh		prepare-for-afp.sh

Provide feedback