Advertisement

Verification of Compilers

  • Gerhard Goos
  • Wolf Znnmerrnaun
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)

Abstract

We report about it joint project of the universities at Karlsruhe, Kiel and Ulm on how to get correct compilers for realistic programming languages. Arguing about compiler correctness must start from a compiling specification describing the correspondence of source and target language in formal terms. We have chosen to use abstract state machines to formalize this correspondence. This allows us to stay with traditional compiler architectures for subdividing the compiler task. A main achievement is the use of program checking for replacing large parts of compiler verification by the much simpler task of verifying program checkers.

Keywords

Register Allocation Assembly Code Transformation Optimization Abstract State Machine Correct Translation 
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. Blum and S. Karman. Program correctness checking... and the design of programs that check their work. In Proceedings 21st Stnnpoeuuti on Theory of Computing, 1989.Google Scholar
  2. 2.
    M. Blum, M. Luby, and R. Rubinfeld. Self-testingycorrecting with applications to numerical problems. In Proceedings 22nd Symposium on Theory of Computing, 1990.Google Scholar
  3. 3.
    Manuel Blum and Sampath Karman. Designing programs that check their work. Journal of the ACM; 42(1):269–291, January 1995.zbMATHCrossRefGoogle Scholar
  4. 4.
    E. Borger, G. Del Castillo, P. Glavan, and D. Rosenzweig. Towards a Mathematical Specification of the APElOO Architecture: the APESE Model. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress volume I: Technology/Foundations, pages 396–401, Elsevier, Amsterdam, the Netherlands, 1994.Google Scholar
  5. 5.
    E. Börger and I. Durdanovic. Correctness of compiling occam to transputer. The Computer Journal, 39(1):52–92, 1996.CrossRefGoogle Scholar
  6. 6.
    E. Börger and I. Durdanovic. Correctness of Compiling Occam to Transputer code. The Computer Journal, 39:52–93, 1996.CrossRefGoogle Scholar
  7. 7.
    E. Börger, I. Durdanovic, and D. Rosenzweig. Occam: Specification and Compiler Correctness.Part I: The Primary Model. In U. Montanari and E.-R. Olderog, editors, Proc. Procomet'94 (IFIP TC2 VVorking Conference on Proqmmminq Concepts, Methods and Calculi). North-Holland, 1994.Google Scholar
  8. 8.
    E. Börger and S. Mazzanti. A Practical Method for Rigorously Controllable Hardware Design. In J.P. Bowen, M.B. Hinchey, and D. Till, editors, ZUM'91: The Z Formal Specification Notation, volume 1212 of LNCS, pages 151–187. Springer, 1997.CrossRefGoogle Scholar
  9. 9.
    E. Börger and D. Rosenzweig. The WAM-definition and Compiler Correctmese. North-Holland Series in Computer Science and Artificial Intelligence. Beierle, L.C. and Pluemer, L., 1994.Google Scholar
  10. 10.
    E. Börger and W. Schulte. A Modular Design for the Java VM architecture. In E. Borger, editor, Architecture Design and Validation Methods. Springer, 1998.Google Scholar
  11. 11.
    E. Börger and W. Schulte. Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. In 23rd international Symposium on Motbcouuicol Foundations of Computer Science, LNCS. Springer, 1998. To appear.Google Scholar
  12. 12.
    E. Börger and W. Schulte. Programmer Friendly Modular Definition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998.Google Scholar
  13. 13.
    D. F. Brown, H. Moura, and D. A. Watt. Actress: an action semantics directed compiler generator. In Compiler Compilers 92, volume 641 of LNCS, 1992.Google Scholar
  14. 14.
    B. Buth, K.-H. Buth, M. Franzle, B. v. 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. volume 641 of LNCS. Springer-Verlag, 1992.Google Scholar
  15. 15.
    B. Buth and M. Müller-Olm. Provably Correct Compiler Implementation. In Tutorial Material-Formal Methods Europe '93, pages 451–465, Denmark, April 1993. IFAD Odense Teknikum.Google Scholar
  16. 16.
    Stephan Diehl. Senuuitics-Dlrected Generation of Compilers and Abstract Machines. PhD thesis, Univeraität des Saarlandes, Germany, 1996.Google Scholar
  17. 17.
    A. Dold, T. Gaul, W. Coerigk, G. Coos, A. Heberle F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeiffer, H. Ruess, and W. Zimmermann. The semantics of a while language ISo. Working paper, The VERIFIX Group, July '95, 1995.Google Scholar
  18. 18.
    H. Emmelmann, F.-W. Schröer, and R. Landwehr. Beg a generator for efficient back ends. In ACM Proceedings of the Sigplan Conference on Programming Language Design and Implementation, June 1989.Google Scholar
  19. 19.
    David A. Espinosa. Semantic Lego. PhD thesis, Columbia University, 1995.Google Scholar
  20. 20.
    T. Gaul, A. Heberle, W. Zimmermann, and W. Goerigk. Construction of Verified Software Systems with Program-Checking: An Application To Compiler Back-Ends. In Proceedings of the Federated Loqics Conference (FloC99) VVorkshop on Runtime Result verification,Trento, Italy, 1999. Electronic Proceedings, URL:http://afrodite.itc.it:1024/~leaf/rtrv/proc/proc.html.
  21. 21.
    T.S. Gaul. An Abstract State Machine Specification of the DEC-Alpha Processor Family. Verifix Working Paper [Verifix/UKA/41], University of Karlsruhe, 1995.Google Scholar
  22. 22.
    Wolfgang Coerigk, Thilo Gaul, and Wolf Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS'98 VVorkshop on “Tool Support for System Specification, Development, and Verificationt”, Advances in Computing Science, Malente, 1998. Springer Verlag. Accepted for Publication.Google Scholar
  23. 23.
    Gerhard Goos. Sather–k —the language. Software —Concepts and Tools, 18: 91–109, 1997.Google Scholar
  24. 24.
    Y. Gurevich. Evolving Algebras: Lipari Guide. In E. Borger, editor, Specification and Validation Methode. Oxford University Press, 1995.Google Scholar
  25. 25.
    Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. In CSL '92, volume 702 of LNCS, pages 274–308. Springer-Verlag, 1993Google Scholar
  26. 26.
    A. Heberle, T. Gaul, W. Coerigk, G. Coos, and W. Zimmermann. Construction of Verified Compiler Front-Ends with Program-Checking. In Proceeduiqe of PSI '99: Andrei Erehou Third International Conference on Perspectiues Of System Infotmatics, pages 370–377, Novosibirsk, Russia, 1999.Google Scholar
  27. 27.
    Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix/UKA/2 revised], IPD, Univeraität Karlsruhe, January 1998.Google Scholar
  28. 28.
    C.A.R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta informatica, 30:701–739, 1993zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    J. Huggins and D. Van Campenhout. Specification and Verification of Pipelining in the ARM2 RISC Microprocessor. ACM Transactions on Design Automation of Electronic System, 3(4):563–580, October 1998.CrossRefGoogle Scholar
  30. 30.
    T.M.V. Janssen. Algebraic translations, correctness and algebraic compiler construction. Theoretical Computer Science, 199:25–56, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  31. 31.
    P. W. Kutter and A. Pierantonio. Montages specifications of realisitic programming languages. Journal of Uniuersol Computer Science, 3(5):416–442, 1997.zbMATHMathSciNetGoogle Scholar
  32. 32.
    John McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Schwartz, pages 33–41.Google Scholar
  33. 33.
    J S. Moore. Piton, MEchanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.Google Scholar
  34. 34.
    P. D. Mosses. Abstract semantic algebras. In D. Bj∅rner, editor, Formal description of programming concepts II, pages 63–88. IFIP IC-2 Working Conference, North Holland, 1982.Google Scholar
  35. 35.
    P. D. Mosses. Action Semantics. Cambridge University Press, 1992.Google Scholar
  36. 36.
    Markus Müller-Olm.An Exercise in Compiler Verification. Internal report, CS Department, Univeraität Kiel, 1995.Google Scholar
  37. 37.
    Markus Müller-Olm. Modular Compiler Verification, volume 1283 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  38. 38.
    J. Palsberg. An automatically generated and provably correct compiler for a subset of ada. In IEEE International Conference on Computer Language, 1992.Google Scholar
  39. 39.
    Jens Palsberg. Provably Correct Compiler Generation. PhD thesis, Department of Computer Science, University of Aarhus, 1992. xii+224 pages.Google Scholar
  40. 40.
    L. Paulson. A compiler generator for semantic grammars. PhD thesis, Stanford University, 1981.Google Scholar
  41. 41.
    A. Pnueli, M. Siegel, and E. Singermann. Translation validation. In Tools and Algorithms for the Construction and Analysis of System, volume 1384 of Lecture Notes in Computer Science pages 151–166. Springer-Verlag, 1998.CrossRefGoogle Scholar
  42. 42.
    Amir Pnueli, O. Shtrichman, and M. Siegel. The code validation tool (cvt). Int. J. on Software Tools for Technology Transfer, 2(2):192–201, 1998.zbMATHCrossRefGoogle Scholar
  43. 43.
    W. Polak. Compiler Specification and Verification, volume 124 of LNCS. Springer-Verlag, Berlin, Heidelberg, New York, 1981.zbMATHGoogle Scholar
  44. 44.
    T. Rus. Algebraic processing of programming languages. Theoretical Computer Science, 199:105–143, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  45. 45.
    J. T. Schwartz, editor Mathematical Aspects of Computer Science, Proc. Symp. in Appl.:Math., RI, 1967. Am.:Math. Soc.Google Scholar
  46. 46.
    Ken Thompson. Reflections on Trusting Trust. Communications of the ACM, 27(8):761–763, 1984.CrossRefGoogle Scholar
  47. 47.
    M. Tofte. Compiler Generators. Springer-Verlag, 1990.Google Scholar
  48. 48.
    C. Wallace. The Semantics of the C++Programming Language. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.Google Scholar
  49. 49.
    M. Wand.A semantic prototyping system. SIGPLAN Notices, 19(6):213–221, June 1984. SIGPLAN 84 Symp. On Compiler Construction.CrossRefGoogle Scholar
  50. 50.
    Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826–849, November 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  51. 51.
    W. Zimmermann and T. Gaul. An Abstract State Machine for Java, Byte Code. Verifix Working Paper [Verifix/UKA/121, University of Karlsruhe, 1997.Google Scholar
  52. 52.
    W. Zimmermann and T. Gaul. On the Construction of Correct Compiler Back-Ends: An ASM Approach. Journal of Universal Computer Science, 3(5):504–567, 1997.zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Gerhard Goos
    • 1
  • Wolf Znnmerrnaun
    • 1
  1. 1.Fakultät für InformatikUniveraitat KarlsruheGermany

Personalised recommendations