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.