Formal Verification of Hardware and Software Systems

4 credits · College of Engineering catalogue

Advisory Prerequisite: None. Enforced Prerequisite: EECS 270 or EECS 281 or EECS 376; No OP/F; or graduate standing. Minimum grade requirement of “C” for enforced prerequisite. (4 credits) Scalable formal automated reasoning for checking the compliance of a state transition system with its safety requirements. Focus is on application to discrete finite-state systems that model hardware and software as well as infinite-state systems that model distributed protocols. Topics include propositional satisfiability (SAT) and SAT modulo theories (SMT) solving, predicate and data abstraction, and minimal unsatisfiable subset (MUS) extraction. Includes hands-on use of state-of-the-art formal verification tools.