Skip to main content
SpringerLink
Log in

Construction of Verified Compiler Front-Ends with Program-Checking

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1755))

Abstract

This paper describes how program-checking can be used to establish the correctness of a compiler front-end which was generated by unverified compiler construction tools. The basic idea of program- checking is to use an unverified algorithm whose results are checked by a verified component at run time. The approach not only simplifies the construction of a verified compiler front-end because checking the result of the analysis is much simpler to verify than the verification of a high sophisticated compiler front-end. It even allows to define a notion of front-end correctness. Furthermore, we are still able to use existing generators ools without major modifications. Additionally, this work points out the tasks which still have to be verified and it discusses the exibility of the approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Börger and I. Durdanovic. Correctness of Compiling Occam to Transputer code. The Computer Journal, 39:52–93, 1996.

    Article  Google Scholar 

  2. Manuel Blum and Sampath Kannan. Designing programs that check their work. Journal of the Association for Computing Machinery, 42(1):269–291, January 1995

    MATH  Google Scholar 

  3. 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 

  4. A. Dold, T. Gaul, W. Goerigk, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Definition of the Language IS. Verifix Working Paper [Verifix/UKA/1], University of Karlsruhe/Kiel/Ulm, 1995.

    Google Scholar 

  5. A.[Dold, T.[Gaul, V.[Vialard, and W.[Zimmermann. H. Schmitt, editors, Proceedings of the 5th International Workshop on Abstract State Machines, pages 50–67, 199

    Google Scholar 

  6. Stephan Diehl. Semantics-Directed Generation of Compilers and Abstract Machines. PhD thesis, University of the Saarland, Germany, 1996.

    Google Scholar 

  7. W. Goerigk, A. Dold, T. Gaul, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Compiler Correctness and Implementation Verification: The Verifix Approach. In P. Fritzson, editor, Proceedings of the Poster Session of CC’96-International Conference on Compil er Construction, pages 65–73. ida, 1996. TR-Nr.: R-96-12.

    Google Scholar 

  8. J. Grosch and H. Emmelmann. A tool box for compiler construction. In Compiler Compilers, Third International Workshop, CC’90; Schwerin, FRG; Proceedings, volume 477 of LNCS. Springer-Verlag, 1990.

    Google Scholar 

  9. J.B. Goodenough and S.L. Gerhart. Toward a Theory of Test Data Selection. SIGPLAN Notices, 10(6):493–510, June 1975.

    Article  Google Scholar 

  10. W. Goerigk, T.S. Gaul, and W. Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS’98 Workshop on “Tool Support for System Speciciation, Development, and Verification”, Advances in Computing Science, Malente, 1998. Springer Verlag.

    Google Scholar 

  11. Gerhard Goos. Sather-K-The Language. Software-Concepts and Tools, 18:91–109, 1997.

    Google Scholar 

  12. A. Heberle and T. Gaul. Syntax einer Sprache zur textuellen Repräsentation von Graphen Interner Bericht, 1998.

    Google Scholar 

  13. Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix/UKA/2 revised], IPD, Universität Karlsruhe, January 1998.

    Google Scholar 

  14. G. C. Necula and P. Lee. The design and implementation of a certifying compiler. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 333–344, 1998.

    Google Scholar 

  15. M. Pettersson. Compiling Natural Semantics. PhD thesis, Linkoeping University, 1995.

    Google Scholar 

  16. Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826–849, November 1997.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Programmstrukturen und Datenorganisation, Universität Karlsruhe, Zirkel 2, D-76128, Karlsruhe, Germany

    Andreas Heberle, Thilo Gaul, Gerhard Goos & Wolf Zimmermann

  2. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Preuβerstr.1-9, D-24105, Kiel

    Wolfgang Goerigk

Authors
  1. Andreas Heberle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thilo Gaul
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wolfgang Goerigk
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gerhard Goos
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Wolf Zimmermann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technology, Technical University of Denmark, Bldg. 244, 2800, Lyngby, Denmark

    Dines Bjøner

  2. Computer Science Department, Technical University of Munich, Arcisstr. 21, 80290, Munich, Germany

    Manfred Broy

  3. A.P. Ershov Institute of Informatics Systems, av. Ac. Lavrentyev 6, Novosibirsk, 630090, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heberle, A., Gaul, T., Goerigk, W., Goos, G., Zimmermann, W. (2000). Construction of Verified Compiler Front-Ends with Program-Checking. In: Bjøner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 1999. Lecture Notes in Computer Science, vol 1755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46562-6_43

Download citation

  • DOI: https://doi.org/10.1007/3-540-46562-6_43

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67102-2

  • Online ISBN: 978-3-540-46562-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation