L15 (11.04.): Proof of program correctness (part 2). Software model checking.