Title: Verification of Hardware and Software.

Various methods for program verification with respect to given

specifications will be covered.

The course consists of two parts.

The first part presents model-checking methods.

The second part introduces deductive methods.

Model-checking: Review of temporal logics as specification languages for reactive properties. The expressive power of temporal logics. The basic algorithms for model checking and  fix-point theory. Automata on infinite words  and their applications to model checking.

Deductive Methods:  Review of Hoare logic, its soundness and (relative) completeness. Recursive procedures: proof under assumptions. Proving properties of nondeterministic programs. Fair termination. Verification of parallel and distributed programs: deadlock freedom, mutual exclusion and progress properties.