Computer-Aided Verification

1 Course Unit

This course introduces the theory and practice of formal methods for the design and analysis of concurrent and embedded systems. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity. Topics: Models and semantics of reactive systems; Verification algorithms; Verification techniques. Topics may vary depending on instructor. Basic knowledge of algorithms, data structures, automata theory, propositional logic, operating systems, communication protocols, and hardware (CIS 2620, CIS 3800, or permission of the instructor). Fall or Spring 1 Course Unit