15-817 Graduate Verification Seminar : Automated Theorem ProvingSpring 2012 Semester
Computer Science Department
Automated Theorem Proving : Coq, Vampire, Z3 - Three very different approaches!
Coq is a powerful proof assistant for higher-order logic, Vampire is the CADE champion resolution theorem prover, Z3 is an SMT solver developed at Microsoft Research that uses efficient decision procedures. It is used for many practic al applications, especially in program analysis.
The primary goal of this course is to develop a working knowledge of Coq. We will cover Z3 and Vampire as time permits according to student interest. However each of these could take a full semester by itself.
- Welcome to 15817!
LecturesWednesday from 3:00 to 4:20 pm in GHC 4102.
Prof. Edmund M. Clarke
Office: GHC 9231
Phone: (412) 268-2628
Office hours: By appointment
Office: GHC 7609
Office: GHC 9229