Exercises and Examples VTSA lecture: Verification of Concurrent and Distributed Software

Marieke Huisman

Luxembourg, July 3 and 4, 2019

• Slides part 1
• power.pvl
• Exercise series 1
  • toZero.pvl
  • zeroAll.pvl
  • LinearSearch
  • BinarySearch
• Solutions to exercise series 1
  • toZero.pvl
  • zeroAll.pvl
  • LinearSearch
  • BinarySearch
• Frame example, with solved version
• Box example
• Lock example
• Exercise series 2
  • SimplePar.pvl
  • fibonacci.pvl
  • LockPar.pvl
  • VerifyThis 2019, Challenge 3
• Solutions to exercise series 2
  • SimplePar.pvl
  • fibonacci.pvl
  • LockPar.pvl (exercise a)
  • LockPar.pvl (exercise c)
  • fibonacci.pvl with counter
• Slides part 2
• Exercise series 3
  • sum_reduction.pvl
  • sequence.pvl
  • VerifyThis 2019, Challenge 3
• Exercise series 4
  • list.pvl
  • tree.pvl
  • swap.pvl
  • owickigries.pvl