@puniko program verification using hoare logic and weakest liberal precondition, linear temporal logic and computation tree logic. (luckily CTL* was removed last minute)