Transcript CSE 599F: Formal Verification of Computer Systems

CSE 599F: Formal Verification
of Computer Systems
Course information
• Instructor: Shaz Qadeer
• Office: 454 Allen Center
• Lectures: CSE 303, Wed-Fri, 12pm1:20pm
• Office hours: Wed-Fri, by appointment
• Web page:
http://www.cs.washington.edu/education/courses/599f/
What is this course about?
• Techniques for improving reliability of
computer systems
– Applicable to both software and hardware
– Focus on software
• Automated techniques for verification
of partial specifications
This course is not about…
• Programming languages and type
systems
• Software engineering methodology
• Dynamic analysis
• Software testing
Prerequisites
•
•
•
•
Algorithms
Formal language theory
Elementary mathematical logic
But, none of that matters if you really
want to understand the material
Goals
• Learn about the fundamental ideas
• Understand the current research
problems
• Do novel research
The best advances come from a combination
of techniques from different research areas!
Grades
• Homeworks
– Work out examples and theoretical problems
– Use prototype verification tools to verify simple
examples
• Discussion and review of research articles
• Project (in groups of 1-2)
– Independent research
– Survey of a research area
– Use a verification tool to verify a realistic system
Why should we care?
• NIST (National Institute of Standards
and Technology) report
– software bugs cost $60 billion annually
• High profile incidents of systems
failure
–
–
–
–
Therac-25 radiation overdoses, 1985-87
Pentium FDIV bug, 1994
Northeast blackout, 2003
Air traffic control, LA airport, 2004
Intellectual challenge
• Civil engineering
– Bridges don’t fail
Reliable Engineering
Intellectual challenge
• Civil engineering
– Bridges don’t fail
• Mechanical engineering
– Cars are reliable
Intellectual challenge
• Civil engineering
– Bridges don’t fail
• Mechanical engineering
– Cars are reliable
• Software engineering
Why is software hard?
• The human element
– Getting a consistent and complete set of
requirements is difficult
– Requirements often change
– Human beings use software in ways never
imagined by the designers
Why is software hard?
• The mathematical element
– Huge set of behaviors
– Nondeterminism
• External due to inputs
• Internal due to concurrency
– Even if the requirements are unchanging,
complete and formally specified, it is
infeasible to check all the behaviors
Bubble Sort
BubbleSort(int[] a, int n)
{
for (i=0; i<n-1; i++) {
for (j=0; j<n-1-i; j++) {
if (a[j+1] < a[j]) {
tmp = a[j];
a[j] = a[j+1];
a[j+1] = tmp;
}
}
}
}
n #inputs
1 2^32
2 2^64
..
..
Even for a small program, enumeration of the set
of all possible behaviors is impossible!
Simple programming language
x  Variable
P  Program =
assert x | x++ | x-- |
P1 ; P2 | if x then P1 else P2 | while x P
Assertion checking for this language is undecidable!
Holy grail of
algorithmic verification
• Soundness
– If the algorithm reports no failure, then
the program does not fail
• Completeness
– If the algorithm reports a failure, then the
program does fail
• Termination
– The algorithm terminates
It is impossible to achieve the holy grail in general!
Methods
• Model checking
• Axiomatic verification
Model checking
• Create a model of the program in a
framework that is decidable
– Finite state system
– Pushdown system
• Manual model creation
• Automated model verification
Axiomatic verification
• Program verification similar to validity
checking in a mathematical logic
– Axioms
– Rules of inference
• Programmer attempts to find a proof
using the axioms and the rules of
inference
• Manual proof discovery
• Automated proof checking
Recently…
• Combination of model checking and
axiomatic verification
– Iterated abstration and refinement