Translation Validation: From Signal to C - Correct System Design: Recent Insights and Advances - page 244

[3] A. Benveniste, P. Le Guernic, and C. Jacquemot. Synchronous programming
with events and relations: the SIGNAL languages and its semantics.

Science of

Computer Programming , 16:103{149, 1991.
[4] E. Borger, E. Gradel, and Y. Gurevich. The Classical Decision Problem . Springer-
Verlag, 1996.
[5] B. Buth, K.-H. Buth, M. Franzle, B. von Karger, Y. Lakhneche, H. Langmaack,
and M. Muller-Olm. Provably correct compiler development and implementation.
In U. Kastens and P. Pfahler, editors, Compiler Construction'92, 4th International
Conference Paderborn, Germany , volume 641 of Lect. Notes in Comp. Sci. , pages
141{155. Springer-Verlag, 1992.
[6] K.M. Chandy and J. Misra. Parallel Program Design: a Foundation . Addison-

Wesley, 1988.
[7] A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra, J. Profeta, D. Romano,
P. Traverso, and B. Yu. A provably correct embedded verier for the certication
of safety critical software. In O. Grumberg, editor, Proc. 9 th Intl. Conference
on Computer Aided Verication (CAV'97) , volume 1254 of Lect. Notes in Comp.
Sci. , pages 202{213. Springer-Verlag, 1997.
[8] A. Cimatti, F. Giunchiglia, P. Traverso, and A. Villaorita. Run-time result
formal verication of safety critical software: an industrial case study. In Run-
Time Result Verication . The 1999 Federated Logic Conference, 1999.
[9] D.L. Clutterbuck and B.A. Carre. The verication of low-level code. Software

Engineering Journal , pages 97{111, 1998.
[10] P. Curzon. A veried compiler for a structured assembly language. In interna-
tional workshop on the HOL theorem Proving System and its applications . IEEE
Computer Society Press, 1991.
[11] J.D. Guttman, J.D. Ramsdell, and V. Swarup. The VLISP veried Scheme system.
Lisp and Symbolic Computation , 8:33{100, 1995.
[12] J.D. Guttman, J.D. Ramsdell, and M. Wand. VLISP: A veried implementation
of Scheme. Lisp and Symbolic Computation , 8:5{32, 1995.
[13] M. Muller-Olm. Modular Compiler Verication: A Renement-Algebraic Ap-
proach Advocating Stepwise Abstraction , volume 1283 of Lect. Notes in Comp.

Sci. Springer-Verlag, 1997.
[14] D.P. Oliva, J.D. Ramsdell, and M. Wand. The VLISP veried PreScheme com-
piler. Lisp and Symbolic Computation , 8:111{182, 1995.
[15] I.M. O'Neill, D.L. Clutterbuck, and P.F. Farrow. The formal verication of safety-
critical assembly code. In IFAC Symposium on safety of computer control systems ,
1988.
[16] Private communications with TNI (BREST), Siemens (Munich) and Inria
(Rennes).
[17] A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas
by small-domains instantiations. In N. Halbwachs and D. Peled, editors, Proc.
11 st Intl. Conference on Computer Aided Verication (CAV'99) , Lect. Notes in
Comp. Sci. Springer-Verlag, 1999. to appear.
[18] A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic
verication. In R. Alur and T. Henzinger, editors, Proc. 8 th Intl. Conference on
Computer Aided Verication (CAV'96) , Lect. Notes in Comp. Sci., pages 184{195.
Springer-Verlag, 1996.
[19] A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT)- auto-
matic verication of a compilation process. Software Tools for Technology Trans-

fer , 2, 1999.