CSCI P415/P515 - Introduction to Verification, Spring 2008

What's New -- Look here regularly for postings
5/5	• Revised grades, scores [PDF], and chart [PDF] have been posted. • The file Eval.txt in your SVN repository contains instructor comments. • Please edit a copy of Permission.txt [TXT] and send it to the instructor. • Some students have asked to see examples of project reports. Here are four: [PDF] Michael D. Adams, Joseph P. Near, and Aaron Kahn. Specification and verification of a file system. [PDF] Daniel Smith and Ramyaa. Proving array reversal. [PDF] N. Mahajan, A. Alshalan, and A. Bawaadam. Proving array reversal algorithm using PVS. [PDF] J. Penery. Proving the correctness of an implementation of ordered binary trees and functions operating on them.
5/3	• Grades, scores [PDF], and chart [PDF] have been posted. More to come on Monday.
4/22	• All homeworks are due by the end of today (Tue, 4/22). Homeworks delivered before last Friday's deadline have priority in grading. • Projects are due at 10:00AM, Tuesday, April 29 (final exam time). Send an email message to the instructor after you have uploaded your final version. All group members should have identical project sub-directories in their repositories. • Bonus credit is awarded for projects turned in early on the following basis: Friday +20%; Saturday +15%; Sunday +10%; Monday +5%; Wednesday (4/30) -25%; Thursday (5/1) -90%. • If you wish to opt for a grade of Incomplete, you must first consult the instructor. I usually allow a 30-day extension to finish course work if it is clearly worthwhile.
4/14	• NOTE: I may be arriving 10-30 minutes late to class on Tuesday, April 15. I suggest that those of you working in groups use the time to outline an informal presentation of your project status, as a means of opening a general discussion of progress and problems.
4/10	• Lecture notes [PDF] and presentation [PDF] from the "Pentium Bug" lecture
4/3	• Wensley's Algorithm [PDF]
3/27	• The material below is also covered in Chapter 9 of the textbook [PDF] • Sequential Programs [PDF] • Inference Rules for STMT Programs [PDF] • Program Proofs [PDF] • Wensley's Algorithm [PDF] • Program Refinement [PDF]
3/20	• Translating Pseudocode to SMV [PDF] • Explicit Model Checking [PDF] • Symbolic Model Checking [PDF]
2/27	• Homework scores [HTM] • DUTs for testing reverse solutions [TGZ] • Homework assignments 8 [HTM], 9 [HTM], and 10 [HTM] have been posted. • Lecture notes on the traffic light controller [PDF] • Lecture notes on interleaving semantics [PDF] • The Island Tunnel Controller problem (not assigned) [HTM] • The Dining Philosopher problem (not assigned) [HTM]
2/27	• Preliminary notes on projects [HTM]
2/25	• Complexity of Verification [PDF] • Computation Tree Model [PDF] [SMV] • The SMV Language (K.L. McMillan, 1999) [PDF]
2/20	• Sorting Tutorial (Lists) [PVS], Sorting Tutorial (Arrays) [PDF] and accompanying PVS examples [PVS], [PRF], • Note on translation [PDF], • Lock Problem [PDF] • PVS challenges (extra credit): Benet's Theorem (lots of algebra) [PDF], [PVS] Logic puzzles (proof by refutation) [PVS] Formulation of Peano Arithmetic (back to basics) [PVS]
2/7	• The deadline for uploading your homework to SVN is noon, Friday, February 8. • (4:45pm) A corrected version of Homework 6 [HTM] has been posted.
1/29	• Section 6.7 of the C241 textbook [PDF] may be of some help in part J.pvs [PVS] of Homework Assignment 4 [HTM]. • Indices of class handouts and presentations have been added to this page.
1/28	• Instructions for uploading homework to SVN [HTM], to be discussed in Tuesday's lecture. • In the AP's Around the World news summary in Today's IDS contains an item that reads, in part, "French bank Societe Generale said Sunday that a trader who evaded all its controls to bet $73.5 billion ... on European markets hacked computers and `combined several fraudulent methods' to cover his tracks, ..."
	Old News

§ Catalog description

P415 Introduction to Verification (3 cr.) P: C311 Tools and techniques for rigorous reasoning about programs and systems. Safety, reliability, security, and other design-critical applications. Decision algorithms. Projects involving the use of automated reasoning tools, such as model checkers, theorem provers, and program transformers.

P515 Specification and Verification (3 cr.) P: C311 or B521. Same as P415

§ General Description

This course introduces methods for performing logical analysis of programs and systems to verify their correctness. It lays a foundation for software engineering in critical applications where a high degree of certainty is needed that the programs realize a specified function or behavior. The broader aim is to show that programming can be done rigorously, when necessary, and is not merely a "craft" based on years of experience. More generally, this course allows students to take a retrospective look at what they have learned in prior classes and tie together concepts that may seem disconnected the first time they are seen.

The course centers on automated tools used in practice to prove properties correctness properties about programs and systems. The emphasis is on gaining exposure and skills in the use of automated reasoning tools in the design process. Participants learn to use two such tools, a theorem proving environment and a model checker, and undertake a project involving the use (or implementation) of these tools. Time permitting we also investigate how these tools work, looking at their underlying algorithms and data structures, as well as the relevant theory. However, the emphasis is on doing, in order to gain insight and motivate theoretical aspects.

An important byproduct of this experience is a fundamental understanding of predicate logic. This knowledge comes "for free" in the sense that it is the medium in which the reasoning tools operate. Thus, comprehension of inference rules and formal proofs is assimilated through their active, computer-validated use.

Throughout the course, participants read and discuss writings related to verification including position papers, accident reports, and general articles about formal methods. The purpose is to develop a perspective on design, the role of verification in practice, the kinds of problems this technology addresses, and the kinds it does not.

§ Topic. This couse explores the use of computer assisted reasoning in design-critical applications, that is, systems for which a high cost is associated with design errors. Examples of design-critical systems include, safety critical systems (e.g. avionics, rail signalling, chemical and nuclear monitoring, etc.), medical monitoring, internet banking, communication networks, space probes, as well as also high-volume embedded software and integrated circuits (e.g. microprocessors, cellular telephones, etc.).

Participants learn how to use reasoning tools for specification analysis and implementation verification, examine the underlying algorithms and data structures for high performance decision procedures, and survey selected reports, case studies, and essays relating to catestrophic design errors.

Verification is the task of determining whether an implementation satisfies its specification. This has traditionally been done by submitting the design (a program or hardware simulation) to a battery of test inputs and comparing generated with expected outputs. As systems get larger, the number of possible tests is astronmically high, so this experimental style of verification can cover only a tiny fraction of the possibilites. Formal verification is the use of decision procedures to completely characterize a design; it is equivalent to exhaustive testing for a particular property.

In design critical applications, the considerable effort of formal verification is worthwhile; and, as the needed tools and expertise develop, broader classes of design are subject to this methodology. The focus of this course is on the technology of verification, how it is built and used today, and what it will look like in the future.

§ Background.

In general, a wide variety of applicable interests will be present in the class. This course may appeal to students with expertise in systems of both hardware and software, programming methods, concurrency, logic, mechanized reasoning, and others. While much of the topical material is determined, the direction and emphasis is not; it will be depend to a significant degree on the interests of the participants.

Thus, if you have completed the core courses of a computer science/engineering major and have an interest in systems, theory, hardware/architecture, software engineering, logic, programming languages, or have an interest in critical design applications you should consider yourself qualified. Experience indicates that successful people in this field have good mathematical skills and a keen interest in applications.

"Do I need C311?" Because of scheduling issues, a significant number of undergraduate Seniors ask permission to take this course concurrently with C311 (normally a prerequisite). Having tracked these students over the years, I have found that strong students have sufficient aptitudes and experience to succeed (not necessarily with an A) in this course while taking C311 at the same time. The topical content C311 is less significant than the methodogical content. However, I assume in my lectures that all students have an throught understanding of languages, interpretation, functional modelling techniques, and recursive expression.

§ Objectives. The course has five primary objectives, all contributing toward an introductory knowledge of verification and formal methods.

1. Experience in the use of a proof assistant. We will collectively learn the PVS reasoning environment, a proof building tool based on higher order logic and a sequent calculus. (If you have experience with another tool, please see the instructor.)
2. Experience in the use of a model checker. In contrast to the interactive character of theorem proving tools, model checkers provide highly automated proof generation based on decision procedures for restricted forms of logic. In these systems, the challenge is expressing the properties to be verified in terms of these restricted logics. We will use the Cadence SMV system to explore these issues.
3. Applications to specification and verification tasks. We will look at how these various tools are used to attack problems in the field. Successful applications involve expertise in how properties are formally represented, how design instances are reduced to tractable proof problems, and performance factors in the underlying technology. Alternatively, a number of possible projects will arise, any of which may be undertaken.
4. The motivation for formal methods research. We will review articles describing noteworthy design failures and catastrophes and explore whether they might have been averted with more rigorous design methods.
5. Theoretical basis. The relevant mathematics will be introduced as needed. This basis includes automata theory, decision algorithms for finite logic, semantics, and calculi.

Formal analysis does not see widespread use in practice, but areas of application are expanding. It is not my goal to prepare you for a career in verification, or even to convince you that formal verification is "the one true way." Rather, I want you to see that programming can be done rigorously, when it is necessary to do so. For most students, I believe this is an opportunity to consider what they have learned in retrospect, and to begin making sense of programming.

§ Outline. This agenda of course topics and threads is likely to evolve during the course of the semester. I am open to suggestions, so if there is something you would like to see covered, feel free to discuss it with me or bring it up in class. Each item includes my estimate of the cumulative class time it will take to cover the material.

1. Theroem Proving (6 weeks). The PVS system is an interactive tool for building proofs in higher order logic. It is a general tool for formalizing mathematical arguments, which we shall apply to reasoning about programs and their specifications. This is the hardest tool to master, so we will start the course by looking at its basic operation. The PVS documentation is installed at /l/pvs/doc. There is additional documentation on SRI's PVS home page.
2. Model Checking (3 weeks). The SMV system is a model checking tool, an algoritm for deciding whether an automaton satisfies a temporal logic predicate. SMV is designed for the automatic analysis and verification of concurrent programs. The SMV Language Refernce and User Interface documentation are good introductions to the use of SMV. There is also a Tutorial available for those who want to work ahead.
3. Decision Procedures (2 weeks). Although this course does not focus on the underlying algorithms and data structures employed in automated reasoning, some time is devoted to selected instances, in order to give a general sense of the reasoning technology. Students with interests in this area have the option of doing an exploratory implementation project.
4. Program Logics (2 weeks). Program logics provide a symbolic calculus for tying assertions about what a program does to the program itself. Understanding the logical connection enables us to develop programs in a more systematic way---with the aim of constructing correct programs rather than proving programs correct. Lecture notes will be provided when this topic is presented.
5. Recursive functions (2 weeks). We are interested in reasoning about recursive functions both as a program logic (as illustrated in C211 and C311), and as a mathematical tool for understanding logic and semantics. Lecture notes will be provided when this topic is presented.
6. Automata (2 weeks) We will look at basic constructions and results in automata theory as they apply to model checking. Lecture notes will be provided when this topic is presented.

§ Text, Reference Material, etc.

There are no required textbooks. The following references may be useful for students seeking background information or interested in advanced topics.

• Induction, Recursion and Programming, (2007 draft) [PDF] by Steven D. Johnson. This is a draft textbook for CSCI C241. This course parallels its presentation, and assumes general familiarity with its topics and notation. Of particular importance is Chapter 3, which is about the relationship between inductive types, structural induction, and recursive definition. The "applications" chapters on formal logic and proving programs also provide perspective on the topical organization of this course.
• Daniel Solow. How To Read And Do Proofs: An Introduction to Mathematical Thought Processes. (2nd ed.) by Daniel Solow. John Wiley & Sons. For anyone who feels uncomfortable dealing with mathematical arguments---and for many who feel comfortable--- this book is and excellent introduction to proofs and proving in mathematics.
• Logic in Computer Science: Modelling and reasoning about systems by Michael R. A. Huth and Mark D. Ryan. A popular introductory text on formal verification. Its topics augment the lecture material in this class, It also looks at some algorithmic aspects
• Model Checking by Edumnd M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. The MIT Press, 1999. This book give a detailed presentation of semantic and algorithmic aspects of "BDD based" model checking.
• Safeware: System Safety and Computers. Nancy G. Leveson. Addison-Wesley, 1995. "A guide to preventing accidents and losses caused by technology" authored by one of the most knowledgable authorities on safety-critical design methods.
• The History of the Calculus and Its Conceptual Development. Carl D. Boyer. Dover Publications, 1959. A math-science history classic that offers a perspective on the what is (or may be) going on in computing Today.

§ Evaluation. The following activities will determine your grade:

• Homework assignments (approx. 50%), including problems and essays.
• Tests (approx. 20%)
• Project (approx 30%) A significant term project.

Students are strongly encouraged to fill out course evaluations at the end of the semester, and will be given credit equivalent to approximately 2% of the course grade for submitting an evaluation (whose content remains anonymous).

Please review:

• The Computer Science Department Statement on Academic Integrity
• The Computer Science Department Incomplete Policy