Information Technology Reference
In-Depth Information
Module Conjuncts Time (min.)
M1
530
1:54
M2
533
1:30
M3
124
0:27
M4
308
2:22
M5
860
5:55
Total :
2355
12:08
Although it is hard to assess at this stage how strongly this particular ex-
ample indicates the feasibility of the Translation Validation approach, the case
study undoubtedly shows that a compilation process (of the type we consid-
ered) of an industrial size program can be automatically veried in a reasonable
amount of time.
7 Conclusions
We have presented the theory which underlies our translation validation ap-
proach for optimizing industrial compilers from Signal to C. We described the
translation of Signal and C programs to STS, the generation of the substitu-
tion
ref
as they are implemented in CVT (the Code Validation Tool). In addition, the
decision procedure, including the abstraction, the Range Allocation algorithm
and various other optimizations that were not presented in this paper, are also
implemented in CVT. We believe that the case study that was presented in the
paper is a strong indication that translation validation is a viable alternative to
full compiler verication.
and the nal assembling of the proof obligations according to Rule
Dedication This paper is dedicated with friendship and appreciation to Hans
Langmaack, a pioneer in the area of compiler verication, whose work proved
the great value and feasibility of a seamless and fully veried development path
from specication to implementation.
Acknowledgment We wish to express our gratitude to Markus Muller-Olm
who reviewed an earlier version of this article in record-time and yet managed
to provide us with several signicant and insightful comments which led to a
meaningful improvement in the quality and validity of this paper.
References
[1] M. Abadi and L. Lamport. The existence of renement mappings.
Theoretical
Computer Science , 82(2):253{284, May 1991.
[2] W. Ackerman. Solvable cases of the Decision Problem . Studies in Logic and the
Foundations of Mathematics. North-Holland, Amsterdam, 1954.
Search WWH ::




Custom Search