Who can take this course, and why!

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 and/or databases.

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.

Course format

The course is taught as a discussion. There are bi-weekly homeworks, a take-home midterm, and a take-home final. Students will also cooperate in teams on a project using some of the verification software in current use.

Instructor

Prof. Bill Rounds, 132 ATL, 1101 Beal Ave. Phone: 734-764-9418

Text: Huth and Ryan, Logic in Computer Science: Modelling and Reasoning about Systems (second edition). Cambridge University Press.