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.