Read the first part of Lamport’s book on TLA+.

Papers read

  • A Scalable and Oblivious Atomicity Assertion, Guerraoui and Vukolic

Plan for next week

Try to investigate the use of QuickCheck: write a first prototype. Scout theorem provers and formal tools.