CS 8803 Formal Methods
Spring 2003

Class Information

Location: Meeting times: Web page: Oscar info:

CCB 53 Monday/Wednesday, 5:05PM-6:25PM http://www.cc.gatech.edu/~manolios/courses/Formal-methods/2003-Spring/ CS 8803 B 20573

Class Web Pages

Syllabus Homework Assignments Handouts

Tools Announcements Reading List

Course Description

Why would you want to take this class?

• You are interested in the foundations of computation and want answers to questions such as:

  • What rules govern the behavior of computation?
  • How do we specify requirements for systems and verify that they are met?
  Formal methods form the foundations of software, security (along with cryptography), and, more generally, computation. Formal methods are based on logic, which (along with set theory) forms the foundation of all of mathematics.

• You are interested in how to use one computing system to reason about another. The sheer complexity of systems makes it impossible to reason about them without assistance from another computing system. The theoretical and practical questions that arise can provide several lifetimes worth of intellectual challenges. For example, how efficiently can we reason about propositional logic, the simplest of all logics? This is essentially the famous P=NP problem.

• You are interested in building dependable systems. Computing systems are ubiquitous, controlling everything from cars and airplanes to financial markets and the distribution of information. Many of these systems interact with changing environments in complex ways that are often not fully understood and which sometimes lead to disastrous consequences, economic and otherwise. The recent PITAC (President's Information Technology Advisory Committee) report makes it clear that building dependable software systems is one of the major challenges facing the computing field.

  We have become dangerously dependent on large software systems whose behavior is not well understood and which often fail in unpredicted ways.

  Formal methods applied to the design and testing phases of development can be practical and economical as they enable one to exhaustively check parts of a design, often revealing the presence of subtle bugs that would otherwise go undetected. Industry is starting to notice, with companies such as Intel, IBM, AMD, Microsoft, Motorola, Cadence, Synopsis, etc. all engaged in efforts to build reliable systems using formal methods.

Teaching Philosophy

My goal is to help you develop into critical, independent-thinking, and creative scientists. In this course, I will try to do this by selecting material that I expect will be relevant for most of your careers and by giving you opportunities to grapple with and gain technical mastery of some of the most important ideas in formal methods. You gain technical mastery by doing and, for the most part, this occurs outside of the class. My role is to create the opportunity for learning; it is only with your active participation that learning truly takes place.

During lectures I try to explain, clarify, emphasize, summarize, encourage, and motivate. I can also answer questions, lead discussions, and ask questions. In class you have an opportunity to test your understanding, so things work best if you come to class prepared. We can then focus on the interesting issues, rather than on covering material that you could just as easily find in the book.

Questions?

Last modified: Sat Jan 25 10:40:18 EST 2003