15-817 Graduate Verification Seminar : Automated Theorem Proving

15-817 Graduate Verification Seminar : Automated Theorem Proving

Spring 2012 Semester
Computer Science Department

Course Description

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!


Wednesday from 3:00 to 4:20 pm in GHC 4102.

Contact Information


Prof. Edmund M. Clarke
Office: GHC 9231
Phone: (412) 268-2628
Office hours: By appointment

Teaching Assistants

Soonho Kong
Office: GHC 7609
Phone: 412-268-3076

Course Secretary

Denny Marous
Office: GHC 9229
Phone: 412-268-7660