Information Technology Reference
In-Depth Information
l
=1
∧ x
=0
→ l
:= 2
while (x != 0) {
if (x % 2 == 0) {
x=x-2;
} else {
x=3*x+1;
[]
l
=1
∧ x
=0
→ l
:= 8
[]
l
=2
∧ x
mod 2 = 0
→ l
:= 3
[]
l
=2
∧ x
mod 2
=0
→ l
:= 5
[]
l
=3
→ x
:=
x −
2
,l
:= 7
[]
l
=5
→ x
:= 3
x
+1
,l
:= 7
}
[]
l
=7
→ l
:= 1
}
Fig. 1.
A C program (left) and the equivalent program in the guarded command lan-
guage (right)
2.2 Detecting Errors in Programs
Automatic program verification aims to determine properties valid for all or some
of the possible executions of a program. In this paper we consider a specific
instance of the automatic verification problem, which aims to determine the
specific class of
reachability
properties. A reachability problem can be stated as
follows: Given a program
p
,aset
I
⊆
S
of
initial states
and a set
O
⊆
S
of
correct states
, determine whether or not the reachable state space of
p
is entirely
contained in the set of correct states.Informalterms,wewanttodetermine
whether there exist
s
O
such that
s
p
∗
s
. The complement of
∈
I
and
s
/
∈
→
O
is the set of the
failure states
.
(Un)reachability properties are a kind of
safety
properties. Safety properties
state that during any possible program computation “something bad” never
happens. More formally, a computation violates a safety property if there is
a finite prefix (“something bad”) which is not shared with at least one other
computation that does not violate it. In the case of reachability this happens
whenever a computation hits a failure state. In this case we say that the program
under analysis is
incorrect
w.r.t. the property, and
correct
otherwise.
A
(verification) technique
is a procedure that takes as input a program
p
and two specifications of the sets
I
and
O
, and tries to decide whether an error
state is reachable from a state in
I
. Being reachability undecidable in the gen-
eral case, a verification technique does not produce a conclusive answer on all
combinations of its inputs. To account for this we consider as possible answers
one of
CORRECT
,
INCORRECT
,
INCONCLUSIVE
, meaning that
p
is correct, incorrect
w.r.t. the reachability problem, and that the technique has failed in deciding
about correctness, respectively. Some techniques are
partial
, i.e., they diverge
on some possible inputs. Additionally, we assume that a technique is always
sound
with respect to both
CORRECT
and
INCORRECT
—i.e., whenever a technique
returns
CORRECT
(respectively,
INCORRECT
), the program is indeed correct (re-
spectively, incorrect). This is equivalent to assuming that there is no discrepancy
between the true program semantics and the semantics assumed by the technique
when it reasons about the program—an assumption that often does not hold in
Search WWH ::
Custom Search