All Projects → vrahli → Velisarios

vrahli / Velisarios

Licence: GPL-3.0 license
A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems

Programming Languages

Coq
218 projects
ocaml
1615 projects
Makefile
30231 projects

Compilation

The code compiles with Coq version 8.9.0. To compile the code, first generate a Makefile by running ./create-makefile.sh. Then type make -j X, where X is the number of jobs you want to use.

Note that create-makefile.sh requires a version of base >= 4.

Roadmap

  • The model is in model.
  • Our formalization of PBFT is in PBFT.
  • Our runtime environment is in runtime.

Running

To run PBFT, check out runtime/README.md.

Authors

  • Vincent Rahli
  • Ivana Vukotic
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].