Case Studies and Parameters in Parameterized Distributed Systems

  • D1.1 Case studies: hosted in the repository.
  • D1.2 Presentation and analysis of the case studies (version of March 2018).


Examples and codes are hosted at InriaForge.

Work in progress

  • Cubicle with asynchronous channels: hosted on github (branch "channels").
  • Cubicle to TLA+: translation of a Cubicle model to a TLA+ specification, hosted on github.
  • Framework TLA+ for the specification and the verification of distributed systems. Online (old version), work in progress.
  • Verification of communication-parametric BPMN collaborations: website, github repository.


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.