CS 6862 |
Formal Methods and Automated Reasoning |
Spring 2011 |
OverviewThis 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. Instructor: Robert Constable Time: Tue/Thu 10:10-11:25am Location:
|
Announcements |
Administration |
Resources
|