Translation Validation: From SIGNAL to C
Translation validation is an alternative to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program. In order to be a practical alternative to compiler verification, a key feature of this validation is its full automation.
Since the validation process attempts to “xunravel” the transformation effected by the translators, its task becomes increasingly more difficult (and necessary) with the increase of sophistication and variety of the optimizations methods employed by the translator. In this paper we address the practicability of translation validation for highly optimizing, industrial code generators from Signal, a widely used synchronous language, to C. We introduce new abstraction techniques as part of the automation of our approach.
KeywordsAtomic Formula Proof Obligation Industrial Case Study Abstract Variable Signal Program
Unable to display preview. Download preview PDF.
- W. Ackerman. Solvable cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954.Google Scholar
- E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag,1996.Google Scholar
- B. Buth, K.-H. Buth, M. Fränzle, B. von Karger, Y. Lakhneche, H. Langmaack, and M. Müller-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.Google Scholar
- K.M. Chandy and J. Misra. Parallel Program Design: a Foundation. Addison-Wesley, 1988.Google Scholar
- A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra, J. Profeta, D. Romano, P. Traverso, and B. Yu. A provably correct embedded verifier for the certification of safety critical software. In O. Grumberg, editor, Proc. 9th Intl. Conference on Computer Aided Verification (CAV‘97), volume 1254 of Lect. Notes in Comp. Sci., pages 202–213. Springer-Verlag, 1997.Google Scholar
- A. Cimatti, F. Giunchiglia, P. Traverso, and A. Villafiorita.Run-time result formal verification of safety critical software: an industrial case study. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999.Google Scholar
- D.L. Clutterbuck and B.A. Carre. The verification of low-level code. Software Engineering Journal, pages 97–111, 1998.Google Scholar
- P. Curzon. A verified compiler for a structured assembly language. In international workshop on the HOL theorem Proving System and its applications. IEEE Computer Society Press, 1991.Google Scholar
- M. Müller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, volume 1283 of Lect. Notes in Comp. Sci. Springer-Verlag, 1997.Google Scholar
- I.M. O‘Neill, D.L. Clutterbuck, and P.F. Farrow. The formal verification of safetycritical a ssembly code. In IFAC Symposium on safety of computer control systems, 1988.Google Scholar
- Private communications with TNI (BREST), Siemens (Munich) and Inria (Rennes).Google Scholar
- A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small-domains instantiations. In N. Halbwachs and D. Peled, editors, Proc. 11st Intl. Conference on Computer Aided Verification (CAV‘99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999. to appear.Google Scholar
- A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, Proc. 8 th Intl. Conference on Computer Aided Verirication (CAV‘96), Lect. Notes in Comp. Sci., pages 184–195. Springer-Verlag, 1996.Google Scholar
- A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT)-automatic verification of a compilation process. Software Tools for Technology Transfer, 2, 1999.Google Scholar
- A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In B. Steffen, editor, 4th Intl. Conf. TACAS‘98, volume 1384 of Lect. Notes in Comp. Sci., pages 151–166. Springer-Verlag, 1998.Google Scholar
- A. Stump and D. Dill. Generating proofs from a decision procedure. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999.Google Scholar
- P. Traverso and P. Bertoli. Mechanized result verification: an industrial application. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999.Google Scholar