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.

Announcements

• Welcome to 15817!

Lectures

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

Contact Information

Instructors

Prof. Edmund M. Clarke emc...@cs.cmu.edu Office: GHC 9231 Phone: (412) 268-2628 Office hours: By appointment

Teaching Assistants

Soonho Kong soon...@cs.cmu.edu Office: GHC 7609 Phone: 412-268-3076

Course Secretary

Denny Marous dcm...@cs.cmu.edu Office: GHC 9229 Phone: 412-268-7660