This course will cover a number of techniques that have proven to be useful in verifying software and hardware systems including Temporal Logic, Model Checking, BDDs, Fast SAT Procedures, and Theorem Proving. The focus of the course will be on the PVS Theorem Prover / Model Checker developed at SRI (and widely regarded as the most powerful tool in its class). Students will learn how to use PVS for hardware and software verification. Some of the basic decision procedures used in PVS for theorem proving and model checking will be presented. The course will conclude with a discussion of the limitations of PVS for software and hardware verification and how a tool might be constructed that would be more powerful.

Schedule: Wednesday 3:00-4:30

Location: NSH 1507

The course will count as 6 graduate course credits.