Information Technology Reference
In-Depth Information
in one of the subclasses of Button . The proof is constructed automatically in
KeY with 161 nodes and 10 branches in the proof tree.
In a second experiment, we interleave symbolic execution and partial evalu-
ation to prove the same claim. The partial evaluator propagates with the help
of the Type Inference rule in the previous section the information that the run-
time type of button is RadioButtonX11 and the only possible implementation of
button . paint () is RadioButtonX11 . paint (). All other possible implementations
are pruned. Only 24 nodes and 2 branches occur in the proof tree when running
KeY integrated with a partial evaluator.
6 Evaluation
Java
We implemented a simple partial evaluator for
and interleaved it with
symbolic execution in the KeY system as described above. We formally verified
anumberof
Java
programs with KeY with and without partial evaluation.
Table 1 shows the experimental results for a number of small
programs
which can be found in the KeY distribution. The column “Program” shows
the name of the program we prove, the column “Strategy” shows the strat-
egy we choose to perform the proof where “SE” means symbolic execution and
“SE+PE” means interleaving symbolic execution and partial evaluation; the
column “#Nodes” shows the total number of nodes in the proof; the column
“#Branches” shows the total number of branches in the proof. The results show
that interleaving symbolic execution with partial evaluation significantly speeds
up the proof for complexEval , constantPropagation , dynamicDispatch , safe-
Access ,and safeTypeCast which can all be considered to be amenable for
partial evaluation. Table 2 shows the experimental results of verifying a larger
and more realistic
Java
e-banking application used in [3, Ch. 10]. The column
“Proof Obligation” shows which property we prove; the remaining columns are
as in Table 1. The results show that symbolic execution interleaved with partial
evaluation can speed up verification proofs even for larger applications. As is
Java
Table 1. Symbolic execution and partial evaluation for small Java programs
Program
Strategy #Nodes #Branches
SE
261
15
complexEval
158
3
SE+PE
SE
65
1
constantPropagation
56
1
SE+PE
SE
161
10
dynamicDispatch
SE+PE
24
2
113
4
SE
methodCall
108
3
SE+PE
28
4
SE
safeAccess
SE+PE
24
3
73
5
SE
safeTypeCast
SE+PE
45
3
 
Search WWH ::




Custom Search