Seminar on deductive and interactive verifiers for establishing program correctness