Deliverables

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).

Repository

Examples and codes are hosted at InriaForge.

Work in progress

Cubicle with asynchronous channels: hosted on github (branch "channels").

Foundations

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.