♦ CSCI P415/515 Tue Sep 27 11:43:56 EDT 2011 [SDJ]

CSCI-P 415 – Introduction to Verification, Spring 2012
CSCI-P 515 – Specification and Verification, Spring 2012

Index        news     info     homework     notes     description     topics     background     text     goals     grading    
What's New -- Look here regularly for postings
may 7, 2012
• Homework scores [PDF] and a chart [PDF]
Course Information
Course: P415 Introduction to Verification (3 cr.) P: C311† or C521†. 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 C521†. 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.
Credit not given for both P415 and P515.
†If you have not taken the prerequisite course, you may still be allowed to enroll. Contact the instructor. See also the Background section below.
Lectures: Tue/Thu 1:00 PM – 2:15 PM, Ballentine Hall (BH) 005
Instructor: Steve Johnson (sjohnson@cs.indiana.edu)
office hours: Tue/Thu 2:30 PM – 3:30 PM, Lindley Hall 330F
Students are welcome in my office any time my door is open
Homework – 10 to 12 weekly assignments & readings. (Due dates are advisory. At certain points in the course, the Instructor will "sweep" your work space to review where you are with the homework. These sweeps are usually announced 4–7 days in advance. Feel free to work ahead, but be advised that some assignments may be changed or extended as the semester progresses.)
 
# due link description
0  A – jan 12
B† – jan 17
C† – mar 13 		[HTM]

[HTM] 		SVN access.
†Parts B and C are optional for P415 students.
  jan 17 [HTM] Reading, Clayton Tunnel Disaster
1  jan 24 [HTM] Homework, Meet PVS
R, 1/26 [HTM] Reading, Patriot Missle Failure
2  M, 1/31 [HTM] Homework, First PVS Exercises
3  T, 2/7 [HTM] Homework, Numerical Induction (See the text book, Ch. 4, for a review)
  T, 2/7 [HTM] Reading, Ariane 5 Missle Failure
4  T, 2/14 [HTM] Homework, Structural Induction (See the text book, Sec. 7.7, for a review)
  R, 2/16 [PDF] Reading, Medical Devices: The Therac 25. (N. Leveson, Safeware: System Safety and Computers, Addison-Wesley, 1995.)
4½  T, 2/21 [HTM] Homework, Synthesis of verification conditions from sequential programs.
5  T, 2/28 [HTM] Homework, Binary Addition, Trees (See the text book, Secs. 2.5 and 6.3)
6 mar 6 [HTM] Abstract Data Type Specification and Implementation
  mar 8 [HTM] Reading, The Pentium™ Bug. No reading is required for this presentation. However, for anyone interested in looking more deeplty into this famous error, a reading list is provided.
7 after
break 		[HTM] List-sorting functions.
8 apr 3 [HTM] [HTM] Meet SMV: Observer-Reporter & Thread-Game problems
9 apr 10 [HTM] Mutual Exclusion Protocols
  mar 29 [HTM] Reading, Mars Climate Orbiter Mishap (See p. 16 for a brief explanation)
  mar 29 [HTM] Reading, Mars Pathfinder Mission
10 apr 26* [HTM] Choice of Final Problems. *Bonus/penalty credit for turning work in early/late. See What's New April 18 entry.
11 Tue, 4/28 In Class Departmental course & instructor evaluations
Notes – There is no required textbook; lecture notes, references, suggersted readings, etc. are posted here
•  SVN [Instructions] for turning in homework
•  PVS [Language] [Prover] [System] [Quick Ref] [Hints] [Prelude]
•  SMV [Old Manual] [VW manual] [Tutorial] [Language]
•  Notes
[PDF]  Terminology
[PDF]  Induction, Recursion, and Programming, draft textbook. Chapters 4, 7, 9, and 10 contain review material relevant to this course.
[PDF]  Complexity of Verification
•  Related readings [HTM]
Project – Up to half of your course grade is based on a project, assigned around the eighth week. Team projects are strongly encouraged.
 
•Information will be posted here later in the semester

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 do assume in my lectures that students have a basic understanding of symbolic programing languages (e.g. Scheme) and recursive programming.

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. However, the emphasis in this course is applications, not theory.

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.

Evaluation.

The following activities will determine your grade:

Individual and group projects are encouraged, and may continue for additional credit subsequent to this course. Such projects may include (but are not limited to) advanced case studies in verification, reeimplementation of tools for either expository or research purposes, integration of software packages in Scheme, and so on. Projects must be approved by the instructor, based on a written proposal as outlined in class.

Participants should expect to work independently to gain expertise with software tools, and creatively to explore applications within their domain of interest. They should expect to share their insights with others and collaborate on more ambitious projects. Although, it is unlikely that one can reach a high level of expertise in a single semester, motivated students will lay the groundwork for experimental research or toward technical skills that currently are in high demand.

Your grade will be determined by:

Students enrolled in the graduate section (P515) are required to do additional work, which may include:

  1. Serving as project leaders for projects involving more than two people.
  2. Importing and presenting a verification tool.
  3. Participation in the development of software for pedagogical use.
  4. Other similar activities.

Students are strongly encouraged to fill out course evaluations at the end of the semester, and will be given credit equivalent to approximately one homework assignment.

Please review: