Syllabus
Office:
Office hours:
Email:
Phone:

CCB 217
Tuesday & Thursday 4:30PM5:30PM, or by appointment
manolios@cc
4048949219

Location:
Meeting times:
Web page:
Oscar info:

CCB (College of Computing) 17
Tuesday/Thursday, 3:05PM4:25PM
http://www.cc.gatech.edu/~manolios/courses/ComputationalLogic/2006Spring/
CS 8803  COL

Course Description
This course covers fundamental aspects of computational
logic, with a focus on how to use logic to verify computing
systems, and can be used as a breadth course for Software
Engineering, Programming Languages, and Information
Security.
Topics covered include firstorder logic, Godel's completeness
and incompleteness theorems, decision problems in FOL, mechanical
verification, modeling computing systems, formal semantics of
programming languages, decision procedures, temporal logic, model
checking, abstraction, and refinement. Students will use the
ACL2 system to model and verify software and hardware
systems. ACL2 consists of a functional programming language, a
logic, and an industrialstrength theorem prover that has been
used to prove some of the largest and most complicated theorems
ever proved about commercially designed systems.
Why would you want to take this class?
Here are three reasons.

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 logic forms the foundations of software, security (along
with cryptography), and, more generally, computation. Logic
(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 based on computational logic.
Teaching Philosophy
My goal is to help you develop into critical,
independentthinking, 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 computational logic. 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.
Textbooks
We will use the following textbooks. All of them are reasonably
priced.

Mathematical Logic, Second Edition. H.D. Ebbinghaus and J.
Flum and W. Thomas. SpringerVerlag, 1994.

ComputerAided
Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother
Moore. Kluwer Academic Publishers, June, 2000. (ISBN: 0792377443)
Note: A paperback version is available on
the
Web. This is much cheaper than the hardcover
version and I have ordered 15 books, so you can buy one
from me.

Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron
A. Peled. MIT Press, 1999. (ISBN: 0262032708)
Also of interest might be:
Before buying any of the following, I suggest that you
evaluate them carefully first.
 For students interested in ACL2 and/or
software/hardware case studies:
 ComputerAided
Reasoning: ACL2 Case Studies. Matt Kaufmann, Panagiotis Manolios, and J
Strother Moore (eds.). Kluwer Academic Publishers, June, 2000. (ISBN: 0792378490)
Note:I have a few copies that I can lend out for
the semester. Also, a paperback version is available on
the
Web. This is much cheaper than the hardcover
version.
 For students interested in the theory of formal methods:

Handbook of Automated Reasoning. In 2 volumes /Editors Alan Robinson
and Andrei Voronkov.  Amsterdam [etc.] : Elsevier ; Cambridge, Mass. MIT Press
(ISBN: 0262182238)
 Term Rewriting and All That. Franz Baader and Tobias
Nipkow. Cambridge University Press, 1998. (ISBN:
0521779200)
 For students interested in security:

Formal Modelling and Analysis of Security Protocols. Peter Ryan
and Steve Schneider. Addison Wesley, 2001. (ISBN: 0201674718)
Grading
Your grade will be based on the following.
Homework:
Grading:
2 Exams:
Projects:

30%
10%
40%
20%

Notes
 Various homework problems will be given, at the approximate
rate of one assignment per every two weeks. Late homeworks will
not be accepted.
 Each problem will be graded in a timely fasion by a class
member, who is also responsible for handing out solutions.
I will review the grading and the solutions you prepare and
will assign a grade based on both the quality and timeliness
of your work. If you grade an assignment,
you do not have to do it and automatically get an A on it,
but I expect you to fully understand it and the solutions
you distribute.
Part of the reason I am asking you to do
this is that I expect you will learn a great deal in the
process, e.g., students often choose to grade
homeworks that are giving them difficulty. In this way, the
impact on their grade is minimized and they get a chance to
really learn the material.
 You are expected to do the homework assignments on your own
without consulting other students or sources other than those
used in class, unless I state otherwise. You can talk to
one another about highlevel ideas and you can consult
sources such as the Web about highlevel ideas, but any
significant insights into assignments gained from any source
should be cited.
The reason I give you homework is to help
you understand the material and yourself. Sometimes things
that seemed obvious in class turn out to be more subtle than
you expected. Homework gives you the opportunity to show,
yourself primarily and me secondarily, that you understand
the concepts and their implications. Sometimes I also ask
that you read and develop some of the concepts on your own.
The material we covered in class should act as the
foundation that makes this possible.
I will also give you opportunities to work in teams.
Some of the homeworks and the project will allow you to work
with other students. I encourage you, but do not require
you, to do this.
 I will give you the exams after class and you will have
until the next day at 5PM to return them to me. I will try
to give you exams that take about 2 hours to complete. This
assumes that you prepared well for them and have
internalized all the main concepts. Please do not expect to
learn what you need while taking the exam; past
experience indicates that this is a bad idea. The reason I
am giving you about a day to complete the exam is that I do
not want you to stess over time constraints. (I feel
compelled to say that as
a graduate student I
found taking tough exams under time constraints a useful experience.)
Here are the rules for the takehome exams. I trust you
to abide by them. Do not consult outside sources when
working on exams. You can use the class textbooks and
handouts that I gave you, but you cannot use any other
source without explicit permission from me. A corollary is
that there should be absolutely no discussion about any of
the exam questions, with anyone other than me.
 The projects can be group projects and can consists of 1, 2,
or 3 people. They have to be cleared by me. During class, I
will toss out project ideas, but feel free to suggest
projects based on your interests. If you are using this
class to fulfill a breadth requirement, then your project
should be in the same area.
Projects will be presented during class. In addition, a single
project report is required. Finally, every member of the team
will evaluate the contributions of the other team members. Your
project grades will be based on the above.
Collaboration on projects is allowed and encouraged.
 You are expected to do the reading before class.
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.
 Academic conduct is subject to the Georgia Tech
Honor Code.
Tentative Syllabus
Here is an overview of the material that I would like to cover.
I reserve the right to make modifications based on the interests
of the class and/or time constraints.
 FirstOrder Logic (FOL)
 Syntax, semantics & model theory for FOL
 Proof theory & its soundness
 Completeness of FOL
 Compactness, LowenheimSkolem, & related theorems
 FOL as the foundations of mathematics
 Undecidability of FOL & arithmetic
 The decision problem
 Godel's incompleteness theorems
 ACL2 (A Computational Logic for Applicative Common Lisp)
 The ACL2 programming language
 Modeling systems & examples from hardware & software
 The ACL2 logic
 Mechanization of ACL2
 Simplification, rewriting & the Boyer/Moore approach to integrating proof techniques
 Verification case studies
 Formal semantics of nondeterministic, imperative programs
 Guarded commands & nondeterminancy
 Partial/total correctness
 Preconditions/Postconditions & Invariants
 Hoare Logic
 Dijkstra's Weakest Precondition Calculus
 Decision Procedures
 DavisPutnamLovelandLogemann SAT algorithm & efficiently decidable cases, including 2SAT & HORNSAT
 BDDs (Boolean Decision Diagrams)
 Linear arithmetic
 Uninterpreted functions & equality
 Combining decision procedures
 Model Checking
 Reactive systems
 Temporal calculi, mucalculus, fixpoints
 Temporal logics (CTL*, LTL, CTL)
 Explicit model checking: algorithms, probabilistic verification & analysis
 Symbolic model checking: algorithms based on BDDs & SAT
 Bounded model checking
 Refinement & Abstraction
 Simulation & bisimulation
 Stuttering, refinement maps, theories of refinement
 Homomorphisms & conservative abstractions
 Abstract interpretation
Last modified: Tue Jan 10 09:46:03 EST 2006