P. Georgiou: "Trace Reasoning in Formal Verification - Guiding Vampire in Induction"; Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-11-22.