Exercise 5 is about program verification with the separation logic tool VeriFast. If you wish you can download and install VeriFast before coming to the session: http://www.cs.kuleuven.be/~bartj/verifast/