CS 8803 Formal Modeling and Analysis of Computing Systems
Spring 2002

Instructor:

Pete Manolios
Office:
Office hours:
Email:
Phone:
260 CRB
Wednesday 12PM-2PM or by appointment
manolios@cc
404-894-9219

Class Information

Location:
Meeting times:
Web page:
S104 Howey-Physics
Tuesday/Thursday, 4:35PM-5:55PM
http://www.cc.gatech.edu/~manolios/courses/Formal-modeling-analysis/2002-Spring/
This course can be used as a breadth course in the Software Engineering and Information Security areas.

Course Description

This course will cover the fundamental techniques for modeling and formally analyzing computing systems, with a focus on applications in software, hardware, and security. Students will learn the fundamentals of classical logic, induction and recursion, program semantics, rewriting, reactive systems, temporal logic, model checking, and abstraction. We will examine how these methods can be used to verify software, hardware, and security protocols. Students will learn how to use various tools, including theorem proving and model checking tools, and will work in groups to apply the tools to various domains. We will discuss the limitations of current techniques and systems and we will examine promising research directions including building more useful systems and developing more powerful techniques.

Grading, Textbooks, and Syllabus

Tools

Homework Assignments

Handouts

Reading List

Announcements

Projects