|Nov 18, 2005|
|Logic and Formal verification
|Term: W 06|
Course No.: EECS 480
Credit Hours: 4
Instructor: Bill Rounds
Prerequisites: EECS 376 or mathematical maturity
EECS 480 is a new course which explores the uses of logic in verifying hardware and software systems. It requires EECS 376, or appropriate mathematical maturity. The course is appropriate for both undergraduates and graduate students, particularly those in software who have an interest in programming languages.
The course focuses on those aspects of logic which have been particularly useful in verifying systems. We look in particular those pieces of logic which have been developed into verifiers, or which have been made into automated theorem proving systems. We look at propositional logic and predicate logic, and then branch into newer kinds of logic such as temporal logic, showing how you can implement these. For example, the temporal logic CTL was developed into the SMV model-checking software and used to verify circuits. We also look at Hoare logic, and we consider efficient data structures like binary decision diagrams.