Progress Meeting

11th july 2017, Paris

Participants: Souheib Baarir, Sylvain Conchon, David Declerck, Lom Hillah, Aurélie Hurault, Alain Mebsout, Stephan Merz, Pascal Poizat, Philippe Quéinnec, Mattias Roux, Fatiha Zaïdi.

Presentations and Discussions

  • Progress on Cubicle "classic" (Alain Mebsout)
  • Progress on Cubicle with weak variables (David Declerck)
  • Cubicle: forward abstracted reachability (Mattias Roux)
  • Translation TLA+ to Cubicle (Stephan Merz) -- slides
  • Case studies and Parameters (Philippe Quéinnec) -- slides
  • Progress on workflow models (Pascal Poizat) -- slides


Minutes of the meeting.

Kickoff Meeting

30th jan 2017 - 1st feb 2017, Toulouse

Participants: Souheib Baarir, Sylvain Conchon, Marie Duflot-Kremer, Mamoun Filali, Lom Hillah, Aurélie Hurault, Philippe Mauran, Stephan Merz, Meriem Ouederni, Pascal Poizat, Philippe Quéinnec, Jean-Baptiste Raclet (partially), Xavier Thirioux (partially), Fatiha Zaïdi.


  • PARDI and the ANR: general information on the ANR (Philippe Quéinnec)
  • Parameters and Distributed Systems
    • Introduction to Distributed Systems (Philippe Quéinnec) - slides
    • Parameters in Distributed Systems (Philippe Quéinnec) - slides
    • Communication Models (Aurélie Hurault) - slides
  • Mechanized Proofs of Parameterized Systems
    • TLA+ and its Tooling (Stephan Merz)
    • Encoding TLA+ into Many-Sorted First-Order Logic (Stephan Merz) - slides (both parts)
  • Automatic Verification of Parameterized Systems
    • Current Status of Cubicle (Sylvain Conchon)
    • Future of Cubicle (Sylvain Conchon) - slides (both parts)
  • Parameterized Workflow Systems
    • Introduction to Workflows (Pascal Poizat) - slides
    • Choreography Development Issues (Pascal Poizat) - slides

Minutes of the meeting

Minutes of PARDI's kick-off (pdf version)