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.
Acknowledgments
We thank the anonymous referees and J. Moore for carefully reading the paper. We are grateful to Hans Langmaack, Friedrich W. von Henke, Axel Dold, Thilo Gaul, Wolfgang Ooerigk, Andreas Heberle, Ulrich Hoffmann, Markus Miiller-Olm, Holger Pfeifer, Harald Rucf and many students in Karlsruhe, Kiel and Ulm for their contributions to the Verifix project which made this paper possible. The Verifix project is supported by the Deutsche Forschungegemeinschaft under contract numbers Go 323/3-2, He 2411/2-2, La 426/15-2.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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.
M. Blum, M. Luby, and R. Rubinfeld. Self-testingycorrecting with applications to numerical problems. In Proceedings 22nd Symposium on Theory of Computing, 1990.
Manuel Blum and Sampath Karman. Designing programs that check their work. Journal of the ACM; 42(1):269–291, January 1995.
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.
E. Börger and I. Durdanovic. Correctness of compiling occam to transputer. The Computer Journal, 39(1):52–92, 1996.
E. Börger and I. Durdanovic. Correctness of Compiling Occam to Transputer code. The Computer Journal, 39:52–93, 1996.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Stephan Diehl. Senuuitics-Dlrected Generation of Compilers and Abstract Machines. PhD thesis, Univeraität des Saarlandes, Germany, 1996.
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.
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.
David A. Espinosa. Semantic Lego. PhD thesis, Columbia University, 1995.
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.
T.S. Gaul. An Abstract State Machine Specification of the DEC-Alpha Processor Family. Verifix Working Paper [Verifix/UKA/41], University of Karlsruhe, 1995.
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.
Gerhard Goos. Sather–k —the language. Software —Concepts and Tools, 18: 91–109, 1997.
Y. Gurevich. Evolving Algebras: Lipari Guide. In E. Borger, editor, Specification and Validation Methode. Oxford University Press, 1995.
Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. In CSL '92, volume 702 of LNCS, pages 274–308. Springer-Verlag, 1993
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.
Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix/UKA/2 revised], IPD, Univeraität Karlsruhe, January 1998.
C.A.R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta informatica, 30:701–739, 1993
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.
T.M.V. Janssen. Algebraic translations, correctness and algebraic compiler construction. Theoretical Computer Science, 199:25–56, 1998.
P. W. Kutter and A. Pierantonio. Montages specifications of realisitic programming languages. Journal of Uniuersol Computer Science, 3(5):416–442, 1997.
John McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Schwartz, pages 33–41.
J S. Moore. Piton, MEchanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.
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.
P. D. Mosses. Action Semantics. Cambridge University Press, 1992.
Markus Müller-Olm.An Exercise in Compiler Verification. Internal report, CS Department, Univeraität Kiel, 1995.
Markus Müller-Olm. Modular Compiler Verification, volume 1283 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
J. Palsberg. An automatically generated and provably correct compiler for a subset of ada. In IEEE International Conference on Computer Language, 1992.
Jens Palsberg. Provably Correct Compiler Generation. PhD thesis, Department of Computer Science, University of Aarhus, 1992. xii+224 pages.
L. Paulson. A compiler generator for semantic grammars. PhD thesis, Stanford University, 1981.
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.
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.
W. Polak. Compiler Specification and Verification, volume 124 of LNCS. Springer-Verlag, Berlin, Heidelberg, New York, 1981.
T. Rus. Algebraic processing of programming languages. Theoretical Computer Science, 199:105–143, 1998.
J. T. Schwartz, editor Mathematical Aspects of Computer Science, Proc. Symp. in Appl.:Math., RI, 1967. Am.:Math. Soc.
Ken Thompson. Reflections on Trusting Trust. Communications of the ACM, 27(8):761–763, 1984.
M. Tofte. Compiler Generators. Springer-Verlag, 1990.
C. Wallace. The Semantics of the C++Programming Language. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.
M. Wand.A semantic prototyping system. SIGPLAN Notices, 19(6):213–221, June 1984. SIGPLAN 84 Symp. On Compiler Construction.
Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826–849, November 1997.
W. Zimmermann and T. Gaul. An Abstract State Machine for Java, Byte Code. Verifix Working Paper [Verifix/UKA/121, University of Karlsruhe, 1997.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Goos, G., Znnmerrnaun, W. (1999). Verification of Compilers. In: Olderog, ER., Steffen, B. (eds) Correct System Design. Lecture Notes in Computer Science, vol 1710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48092-7_10
Download citation
DOI: https://doi.org/10.1007/3-540-48092-7_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66624-0
Online ISBN: 978-3-540-48092-1
eBook Packages: Springer Book Archive