Transcript CSE 599F: Formal Verification of Computer

ECI 2007: Specification and
Verification of ObjectOriented Programs
Lecture 0
Course information
• Instructor: Shaz Qadeer
• Office: Office 19 in this building
• Office hours: 5:30-6:30pm
What is this course about?
• Automated techniques for verification
of partial specifications for software
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
• Enable novel research
The best advances come from a combination
of techniques from different research areas!
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!
Axiomatic progam 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
Program Verification
• Mechanical verification of software would
improve software productivity, reliability,
efficiency
• Such systems are still in experimental stage
– After 40 years !
– Research has revealed formidable obstacles
– Many believed that program verification is dead
“Social processes and proofs of theorems and
programs”, Richard A. DeMillo, Richard J. Lipton,
and Alan J. Perlis, 1977
The research agenda for program
verification is destined to fail.
Criticisms
• Mathematicians do not use automated proof
checkers; they use social processes to check
proofs of theorems
• Program specifications are often as
complicated as the programs themselves
• Many mathematical theories have exponential
or super-exponential proofs; it is
unreasonable to expect that such proofs can
be discovered automatically
Program Verification:
Attack and Defense
• Attack:
– Mathematicians do not use formal methods to
develop proofs
– Why then should we try to verify programs formally?
• Defense:
– In programming, we often lack an effective formal
framework for describing and checking results
– Consider the statements
• The area bounded by y=0, x=1 and y=x2 is 1/3
• By splicing two circular lists we obtain another circular list
with the union of the elements
Program Verification:
Attack and Defense
• Attack:
– Verification is done with respect to a specification
– Is the specification simpler than the program ?
– What if the specification is not right ?
• Defense:
– Developing specifications is hard
– Redundancy exposes many bugs as inconsistencies
– We are interested in partial specifications
• An index is within bounds, a lock is released
Program Verification:
Attack and Defense
• Attack:
– Many logical theories are undecidable or decidable by
super-exponential algorithms
– There are theorems with super-exponential proofs
• Defense:
– Such limits apply to human proof discovery as well
– If the smallest correctness argument of program P is
huge then how did the programmer find it?
– Theorems arising in program verification are usually
shallow but tedious
Program Verification:
Attack and Defense
• Myth:
– Think of the peace of mind you will have when the
verifier finally says “Verified”, and you can relax
in the mathematical certainty that no more errors
exist
• Reality:
– Use instead to find bugs (like more
powerful type checkers)
– We should change “Verified” to “Sorry, I
can’t find more bugs”