cs6964: Theorem Proving
Spring 2008

The goal of cs6964 in Spring 2008 is to provide an introduction to formal specification and verification techniques. The emphasis will be on semantically powerful specification languages coupled with deductive verification techniques. The primary focus of the course is obtaining experience with the construction of solid and useful formal specifications for a variety of CS artifacts (hardware, software, systems, etc.). A secondary focus is the production of formal proofs of system properties, and their automation.

Instructor Konrad Slind (MEB 3436)	Office Hours: Tuesday after class, or by appointment
Class Time Tu/Thu, 10:45-12:05	Class Room MEB 3105

Important Dates

Jan. 8 (First class)
March 17-22 (Spring Break)
March 24-April 4 (Konrad away)
April 22 (Last class)

The University Academic Calendar may be consulted for further information about drop dates and other important dates in the semester.

Topics

Basic Logic	Specification Toolbox	Case Studies
Propositional Logic First Order Logic Higher Order Logic	Basic types Sets N and Recursive types Recursive Functions and Inductive Relations Dealing with Partiality Arrays, Matrices, and Words	Block ciphers Regular Languages Hardware Programming Language Semantics Compilation Abstract Algebra How to write your own proof procedure

Course Materials

The course materials will be a combination of lecture notes, selected research papers, and system tutorials. Here is the current, ever-evolving lecture notes.

You will need to know how to program in SML. If you don't already know it, you will have to learn it on your own, or come to me for some catch-up exercises.

The HOL-4 system will be used to gain experience in various aspects of formalization and theorem proving. The Description, Tutorial, and Logic documents can help in this quest. There is also a SourceForge homepage for this system. The documents are in constant revision; please send me any typos, mistakes, omissions, etc.

Other material of general utility in the area of theorem proving:

Freek Wiedijk's page on symbolic computation systems, including theorem provers. In general, his pages have much interesting content about theorem proving systems.
There are many excellent books on logic. The following is a list of the books that I have. These should all be in the university library.
- Johnstone, Notes on Logic and Set Theory
- Shoenfield, Mathematical Logic
- Devlin, Sets, Functions, and Logic---An Introduction to Abstract Mathematics
- Cori and Lascar, Mathematical Logic (vols 1, 2)
- Crossley et.al, What is Mathematical Logic?
- Barwise (editor), Handbook of Mathematical Logic
- Davis, Computability, Complexity, and Languages
- Moschovakis, Notes on Set Theory
- Halmos, Naive Set Theory
- Davis, Computability and Unsolvability
- Drake and Singh, Intermediate Set Theory
- Shoenfield, Recursion Theory
Please feel free to drop by and borrow some of these books to get other perspectives and alternate explanations of the background.

Grades

Since the aim of the course is to get hands-on experience with a variety of techniques, there will be a few introductory assignments intended to get students up to speed. However, the major component of the course will be a project, to be chosen by the student and approved by the instructor.

Assignments	35%
Project	65%
Total	100%

Assignments and Projects

Assignment 1. Download and build the HOL-4 system from its SourceForge site.
Assignment 2.(answers)
Assignment 3.
A preliminary list of project suggestions is available.I wrote a paper about the projects done by the previous class. The project should be based on the topics and techniques discussed in the course and should represent a substantial formalization and verification effort. You must discuss your project with me before getting started.

Mailing lists

cs6964@cs.utah.edu: You must subscribe to this class mailing list. To subscribe, follow the directions at http://mailman.cs.utah.edu/mailman/listinfo/cs6964

Other Important Information

College of Engineering information for students.
Students with disabilities

Konrad Slind

cs6964: Theorem Proving Spring 2008