Code For Tests Used in "Liveness with Invisible Ranking"

• Channel-Ring
  • Protocol
  • Proof



• Bakery
  • Protocol
  • Proof
  • Assertions



• Bakery with Auxilary Variable
  • Protocol
  • Proof



• Dining philosophers
  • Program
    • DINE(6)
    • DINE(128)
  • Proof
    • Part 1 to generate auxiliary assertions on DINE(6)
    • Part 2 to check premises on DINE(128)
  • Notes
    • how-to-run