# Syllabus

### Pete Manolios

 Office: Office hours: Email: Phone: CCB 217 Tuesday & Thursday 4:30PM-5:30PM, or by appointment manolios@cc 404-894-9219

### Class Information

 Location: Meeting times: Web page: Oscar info: CCB (College of Computing) 17 Tuesday/Thursday, 3:05PM-4:25PM http://www.cc.gatech.edu/~manolios/courses/Computational-Logic/2006-Spring/ 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 first-order 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 industrial-strength 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, 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 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. Springer-Verlag, 1994.
• Computer-Aided Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Kluwer Academic Publishers, June, 2000. (ISBN: 0-7923-7744-3)
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: 0-262-03270-8)

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:
• Computer-Aided Reasoning: ACL2 Case Studies. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore (eds.). Kluwer Academic Publishers, June, 2000. (ISBN: 0-7923-7849-0)
• 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: 0-262-18223-8)
• Term Rewriting and All That. Franz Baader and Tobias Nipkow. Cambridge University Press, 1998. (ISBN: 0-521-77920-0)
• For students interested in security:
• Formal Modelling and Analysis of Security Protocols. Peter Ryan and Steve Schneider. Addison Wesley, 2001. (ISBN: 0-201-67471-8)

 Homework: Grading: 2 Exams: Projects: 30% 10% 40% 20%

### Notes

1. Various homework problems will be given, at the approximate rate of one assignment per every two weeks. Late homeworks will not be accepted.

2. 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.

3. 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 high-level ideas and you can consult sources such as the Web about high-level 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.

4. 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 take-home 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.

5. 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.

6. 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.

7. 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.
1. First-Order Logic (FOL)
• Syntax, semantics & model theory for FOL
• Proof theory & its soundness
• Completeness of FOL
• Compactness, Lowenheim-Skolem, & related theorems
• FOL as the foundations of mathematics
• Undecidability of FOL & arithmetic
• The decision problem
• Godel's incompleteness theorems
2. 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
3. Formal semantics of nondeterministic, imperative programs
• Guarded commands & nondeterminancy
• Partial/total correctness
• Preconditions/Postconditions & Invariants
• Hoare Logic
• Dijkstra's Weakest Precondition Calculus
4. Decision Procedures
• Davis-Putnam-Loveland-Logemann SAT algorithm & efficiently decidable cases, including 2SAT & HORNSAT
• BDDs (Boolean Decision Diagrams)
• Linear arithmetic
• Uninterpreted functions & equality
• Combining decision procedures
5. Model Checking
• Reactive systems
• Temporal calculi, mu-calculus, fixpoints
• Temporal logics (CTL*, LTL, CTL)
• Explicit model checking: algorithms, probabilistic verification & analysis
• Symbolic model checking: algorithms based on BDDs & SAT
• Bounded model checking
6. Refinement & Abstraction
• Simulation & bisimulation
• Stuttering, refinement maps, theories of refinement
• Homomorphisms & conservative abstractions
• Abstract interpretation