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