CSC 7150 Program Analysis and Model Checking (3)

Prereq.: CSC 4890 or CSC 7101 or equivalent. Automata on infinite objects; Buechi Automata; Muller Automata; Rabin Automata; safety and liveness properties; linear temporal logic (LTL), from LTL to automoata; branching time logics; Knaster-Tarski fixpoint theorem; abstract interpretation.