Information Technology Reference
In-Depth Information
Table 2.
Symbolic execution and partial evaluation for an e-banking application
Proof Obligation
Strategy #Nodes #Branches
SE
949
20
ATM.insertCard (EnsuresPost)
SE+PE
805
13
2648
89
SE
ATM.insertCard (PreservesInv)
SE+PE
2501
79
661
7
SE
ATM.enterPIN (EnsuresPost)
654
8
SE+PE
SE
1524
45
ATM.enterPIN (PreservesInv)
1501
44
SE+PE
SE
260
2
ATM.confiscateCard (EnsuresPost)
255
2
SE+PE
739
19
SE
ATM.confiscateCard (PreservesInv)
SE+PE
695
19
1337
35
SE
ATM.accountBalance (EnsuresPost)
SE+PE
1271
29
2233
57
SE
ATM.accountBalance (PreservesInv)
2223
59
SE+PE
SE
16174
136
Account.checkAndWithdraw (EnsuresPost)
17023
135
SE+PE
SE
14076
89
Account.checkAndWithdraw (PreservesInv)
10478
78
SE+PE
to be expected, depending on the structure of the program the benefit varies.
It is noteworthy that none of the programs and proof obligations used in the
present section have been changed in order to make them more amenable to
partial evaluation. In no case we have to pay a significant performance penalty
which seems to indicate that partial evaluation is a generally useful technology
for symbolic execution and should generally be applied.
The case study in Sect. 5 suggests that it could pay off to take partial evalua-
tion into account when designing programs, specifications, and proof obligations.
7 Related Work
Partial evaluation as a technique has been applied in a variety of areas includ-
ing program optimization, compiler generation and meta-compilation. Partial
evaluation has been applied successfully in logic programming [18] as well as
for imperative and object-oriented languages like C [19] and
[14]. A good
overview including many references is given in [2]. As far as we know, the present
paper is the first application of partial evaluation in formal verification.
Our approach is also related to supercompilation [20]. Supercompilation goes
beyond partial evaluation by being able not only to specialize but also to gen-
eralize a program to achieve a functionally equivalent but better performing
program even in the absence of static input.
Java
