Case Studies and Parameters in Parameterized Distributed Systems
Examples and codes are hosted at InriaForge.
PARDI is founded on previous work and software of the partners:
- Cubicle is an open source model checker for verifying safety properties of array-based systems.
- Alt-Ergo is an open source SMT solver dedicated to the proof of mathematical formulas generated in the context of program verification.
- TLAPS: The TLA+ Proof System mechanically checks TLA+ proofs.
- VACS offers automated Verification of Asynchronous Communicating Systems.
- VerChor is a framework for the design and verification of choreographies.
- SChorA is a symbolic choreography analyzer.