Do you mean something specific or his general approach to program correctness i.e. guarded commands, weakest precondition calculus etc. ?