CS 6862

Formal Methods and Automated Reasoning

Spring 2011



This is a course on logic, from the point of view of Computer Science. The driving idea is to use CS background as a lens to look deeply into parts of logic by viewing them in CS terms. The course will focus on aspects of logic that are used in formal methods, an area of CS concerned with how to specify programming tasks and demonstrate that programs and protocols are correct according to their specifications. This area of computer science is critical to computer security, a topic of intense interest to industry and government and one that requires solid knowledge of applied logic.

Topics covered include propositional calculi, predicate calculi, programming logics, Hoare logic, program verification, interactive proof assistants, model checking and other topics in formal methods.


Robert Constable
4147 Upson Hall
Office Hours: Tue and Thu 1:30-2:15 and by appointment.

Time: Tue/Thu 10:10-11:25am