Transcript Document

Using Decision Procedures for
Program Verification
Christopher Lynch
Clarkson University
ICS (I Can Solve)
• ICS is a combination of decision procedures
written by Harald Reuss of SRI
• You can ask ICS if something is satisfiable
• If it is not satisfiable, then it will answer
“unsat”
• If it is satisfiable, then it will give you a
model
Unsatisfiability
• Example 1:
– ics> sat x = 2 & x = 3.
– :unsat
• The prompt is “ics>”
• & means “AND”
• So I asked it whether x = 2 and x = 3 is
satisfiable. Of course x cannot be both 2
and 3, so it answered “unsat”
Unsat Example 2
ics> sat x > 5 & x <= 5.
:unsat
ics> sat x <> 5 & x = 5.
:unsat
ics> sat x < 2 & ~ x < 4.
:unsat
• <> means “not equal” and ~ means “NOT”
Unsat Example 3
ics> sat [x < 5 | x = 5] & x > 5.
:unsat
• | means ”OR” and [ ... ] is used for
parenthesis
• So here I ask if it is satisfiable that x < 5 or
x = 5 and x > 5
Unsat Example 4
ics> sat x > 4 & y > 6 & x + y < 8.
:unsat
ics> sat x = 4 & 3 * x <> 12.
:unsat
Unsat Example (Implication)
• Recall from logic that “p implies q” is
equivalent to ~p | q
ics> sat x = 2 & [~ x = 2 | y = 5] & y <> 5.
:unsat
• This says x = 2 and (x = 2 implies y = 5)
and y <> 5.
Satisfiability
• So far all the example are unsatisfiable
• But if you give it a satisfiable example, then
it will give you back a model
• A model is a value for the variables that
makes the statement true
• Sometimes you must do a bit of work to
understand the model
Sat Example 1
ics> sat [x = 2 | x = 4] & [y = 1 | y = 3] & x + y = 7.
:sat s14
:model [y + x = 7; y = 3;
x = 4]
• I said that x is 2 or 4, and y is 1 or 3, and their sum
is 7, so in the model x is 3, y is 4, and the sum is 7
• S14 is a state here, you get a new state when you
do something new
Sat Example 2
ics> sat x = 2 & y = 4.
:sat s17
:model [x = 2; y = 4]
• This is not very exciting, the model is just
the exact thing I typed
Sat Example 3
ics> sat x > 2.
:sat s18
:model [-2 + x >0]
• Models of inequalities are always
represented this way. x > 2 is represented
by this equation.
Sat Example 4
ics> sat x < 5.
:sat s20
:model [5 + -1 * x >0]
• Convince yourself that this is the right
representation. Remember that
multiplication takes precedence over
addition.
Sat Example 5
ics> sat x = 4 & x >= 4.
:sat s22
:model [-4 + x >=0; x = 4]
• It could have just told me that x = 4, the
other equation is useless. So the user still
has to do some work to figure that out.
Sat Example 6
ics> sat [x = 2 | x = 3] & x < 3.
:sat s23
:model [x = 2; 3 + -1 * x >0]
• Models are mostly useful when you have
OR, because here it figured that x = 2, since
x = 3 won’t work
Sat Example 7
ics> sat x = 2 & [~ x = 2 | y = 5].
:sat s24
:model [x = 2; y = 5]
• Remember this is an implication. Since x =
2, then that implies x = 5, so both must be
true.
Automated Reasoning
• Suppose I want to prove that p implies q
• That means that it is impossible for p to be
true and q to be false at the same time. So
to prove that p implies q, I will prove that p
& ~ q is unsatisfiable
AR Example
ics> sat x > 4 & ~ x > 2.
:unsat
• I wanted to prove that x > 4 implies x > 2.
So I proved that it is unsatisfiable that x > 4
and not x > 2
• Negate the goal and prove unsat
• This is called refutational theorem proving
AR Example 2
ics> sat x = 2 & [~ x = 2 | y = 5] & ~ y = 5.
:unsat
• I wanted to prove that if x = 2 and (x =2
implies y = 5) then y = 5
• So I negated y = 5 and proved unsat
• Refutational Theorem Proving
AR Example 3
ics> sat x = 2 & y = 4 & ~ x + y = 6.
:unsat
• I wanted to show that if x = 2 and y = 4 then
x + y = 6. So I assumed x + y = y and got a
contradiction
• Refutational Theorem Proving
False Theorem
• What if I use refutational theorem proving,
and the theorem is false”
• In that case it returns sat, and gives a model
• The model is a way to make the hypotheses
true and the goal false
False Theorem Example
•
•
•
•
ics> sat [x = 2 | x = 5] & ~ x < 4.
:sat s26
:model [-4 + x >=0; x = 5]
I want to prove that if x = 2 or x = 5 then x
< 4. But that is not true. It gives me the
model where x < 4 and x = 5.
Program Verification
[x = y]
x := x + 1
y := y + 1
[x = y]
• We want to approve that if x = y at the
beginning and this program is run, then x =
y at the end
Annotating the program
[x = y]
[x + 1 = y + 1]
x := x + 1
[ x = y + 1]
y := y + 1
[x = y]
• We propagate the postcondition upward through
the program, applying the assignment statements.
Then we need to prove that the propagated
condition is implied by the precondition
Verifying the Program
ics> sat x = y & ~ x + 1 = y + 1.
:unsat
• We wanted to prove that x = y implies x + 1
= y + 1. We proved refutationally that it is
unsatisfiable that x = 1 and not x + 1 = y +1.
• In other words, we proved the program is
correct.
Another Program
[x = y]
y := x + 1
x := y + 1
[x = y]
• This program is not correct. Let’s see what
happens.
Annotating Program 2
[x = y]
[x + 1 + 1 = x + 1]
y := x + 1
[y + 1 = y]
x := y + 1
[x = y]
Verifying Program 2
ics> sat x = y & ~ x + 1 + 1 = x + 1.
:sat s30
:model [1 + x <> 2 + x; y = x]
• It says sat, so the program is not verified.
For the model, the first condition is
obviously true, so the model is when y = x.
Program 3
[x + y > 2]
x := x + 1
y := y + 1
[x + y > 5]
• This is not necessarily true
Annotating the Program
[x + y > 2]
[x + 1 + y + 1 > 5]
x := x + 1
[x + y + 1 > 5]
y := y + 1
[x + y > 5]
• This is not necessarily true
Verifying the Program
ics> sat x + y > 2 & ~ x + 1 + y + 1 > 5.
:sat s31
:model [-2 + y + x >0; 3 + -1 * y + -1 * x >=0]
• The program is not true, and the model is
when x + y > 2 and x + y <= 3
Program with If
if (x > y)
m=x
else
m=y
[m >= x & m >= y]
Annotating the Program
[(x > y  (x >= x & x >= y)) & ~ x > y  (y >= x &
y >= y))]
if (x > y)
[x >= x & x >= y]
m=x
else
[y >= x & y >= y]
m=y
[m >= x & m >= y]
Verifying the Program
ics> sat ~[[ ~ x > y | [x >= x & x >= y]] &
[~~ x > y | [y >= x & y >= y]]].
:unsat
• Read this carefully, to check that it is right
False If Program
if (x > y)
m=x
else
m=y
[2 * m > x + y]
Annotating the Program
[(x > y  2 * x > x + y) & (~ x > y  2 * y > x +
y)]
if (x > y)
[2 * x > x + y]
m=x
else
[2 * y > x + y]
m=y
[2 * m > x + y]
Verifying the Program
ics> sat ~[[ ~ x > y | 2 * x > x + y] & [~~ x >
y | 2 * y > x + y]].
:sat s33
:model [-1 * y + x >=0; y + -1 * x >=0]
• It says sat, so the program is not correct.
The models says x >= y & y >= x. So we
see the problem is when x = y.