Formal Verification of Pastry

last modified on 24.May.2013 © Tianxiang Lu

Collection of Formal Models for Pastry

This web page collects all the versions of TLA+ models of Pastry and corresponding counterexamples.

Besides, it also provides the TLA+ proofs verifying the improved versions of Pastry.

• CastroPastry
  provides the TLA+ model of Castro04paper and model checking results of it.


• HaeberlenPastry
  provides the TLA+ model inspired by Haeberlen05paper and FreePastry.
  It includes also the model checking results of it.


• HaeberlenSimple
  provides the simplified model of HaeberlenPastry and model checking results of it.


• IdealPastry
  provides the TLA+ model of the first verified Pastry model and also the proof of the property CorrectDelivery with strong (Ideal) assumption.


• IdealPastrySimple
  provides the simplified model of IdealPastry and validation results of it.


• LuPastry
  provides the TLA+ model of the final verified version of Pastry model and also the proof of the property CorrectDelivery with relaxed assumption.


• LuPastrySimple
  provides the simplified model of LuPastry and validation results of it.