CSCI-P 415 – Introduction to Verification, Spring 2012
CSCI-P 515 – Specification and Verification, Spring 2012
|
What's New
-- Look here regularly for postings
|
| feb 14
|
| • |
Revised lecture notes on program inference rules
[PDF]
| | • |
Summary of the PCA rules
[PDF]
| | • |
Example program
[PDF]
| | • |
(Updated after class) Illustrated proof
[PDF]
| | • |
Exercises. Reduce Programs 1–7 to verification conditions.
[PDF]
Due, Tuesday, February 21
|
|
|
|
| jan 31
|
| • |
On Thursday, February 9 I will sweep the SVN repository and grade the homework that is posted there. Be sure to have your area updated by that time.
| | • |
We'll defer the presentation of the Therac 25 reading assignment
for a week or two—but keep reading. The next presentation will
by the Ariane 5 Missle Failure,
which is much briefer and more straightforward.
|
|
| jan 30
|
| • |
Here are the presentation materials from last Thursday's lecture.
Your are not responsible for understanding it yet, but you might want
to start looking at it. If you want to look more deeply, there is
background material in the last chapter of the textbook [PDF], including both formal and informal discussions of the
inference rules.
- The Stmt programing language
[PDF] (updated, 2.14)
- Summary of the Hoare inference rules
[PDF] (updated, 2.14)
- Illustration of verification condition synthesis
[PDF] (updated, 2.14)
|
|
| jan 23
|
|
| jan 10
|
| • |
Read Chapter 3 of the PVS Prover Guide
[PDF]
| | • |
Review the instructions on P415/P515 Homework Procedures
[HTM]
| | • |
Part A of Homework Assignment 0
is due on Thursday, January 12
| | • |
The first reading assignment
is due on Tuesday, January 17.
P515 Students Note: be prepared to present this article to the class.
|
|
| jan 3
|
| • |
If you are interested in working as an AI or UI in the class, contact
the instructor
|
|
|
|
|
|
|
| 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
| |
| Notes – There is no required textbook; lecture notes, references, suggersted readings, etc. are posted here
|
|
|
|
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.
- 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.)
- 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.
- 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.
- 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.
- 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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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. 45%), including problems and essays.
-
Project (approx 45%) A significant term project.
-
Other (0–10%) Including participation, in-class presentations, quizzes, etc.
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:
- the quality of your independent work as demonstrated by
- written reports on the work, and
- your ability to discuss your work and its implications with the
instructor and with the class.
- assigned problems
- your creative contributions to the class and your initiative to
pursue readings and ideas
Students enrolled in the graduate section (P515) are required to do
additional work, which may include:
- Serving as project leaders for projects involving more than two people.
- Importing and presenting a verification tool.
- Participation in the development of software for pedagogical use.
- 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: