Advertisement

Translation Validation: From SIGNAL to C

  • A. Pnueli
  • O. Shtrichman
  • M. Siegel
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)

Abstract

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.

Keywords

Atomic Formula Proof Obligation Industrial Case Study Abstract Variable Signal Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, May 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  2. [2]
    W. Ackerman. Solvable cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954.Google Scholar
  3. [3]
    A. Benveniste, P. Le Guernic, and C. J acquemot.Synchronous programming with events and relations: the SIGNAL languages and its semantics. Science of Computer Programming, 16:103–149, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag,1996.Google Scholar
  5. [5]
    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
  6. [6]
    K.M. Chandy and J. Misra. Parallel Program Design: a Foundation. Addison-Wesley, 1988.Google Scholar
  7. [7]
    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
  8. [8]
    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
  9. [9]
    D.L. Clutterbuck and B.A. Carre. The verification of low-level code. Software Engineering Journal, pages 97–111, 1998.Google Scholar
  10. [10]
    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
  11. [11]
    J.D. Guttman, J.D. Ramsdell, and V. Swarup. The VLISP verified Scheme system. Lisp and Symbolic Computation, 8:33–100, 1995.CrossRefGoogle Scholar
  12. [12]
    J.D. Guttman, J.D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5–32, 1995.CrossRefGoogle Scholar
  13. [13]
    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
  14. [14]
    D.P. Oliva, J.D. Ramsdell, and M. Wand. The VLISP verified PreScheme compiler. Lisp and Symbolic Computation, 8:111–182, 1995.CrossRefGoogle Scholar
  15. [15]
    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
  16. [16]
    Private communications with TNI (BREST), Siemens (Munich) and Inria (Rennes).Google Scholar
  17. [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. 11st Intl. Conference on Computer Aided Verification (CAV‘99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999. to appear.Google Scholar
  18. [18]
    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
  19. [19]
    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
  20. [20]
    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
  21. [21]
    A. Stump and D. Dill. Generating proofs from a decision procedure. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999.Google Scholar
  22. [22]
    P. Traverso and P. Bertoli. Mechanized result verification: an industrial application. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • A. Pnueli
    • 1
  • O. Shtrichman
    • 1
  • M. Siegel
    • 1
  1. 1.Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations