Correct Programs without Proof? On Checker-Based Program Verification

  • Wolfgang Goerigk
  • Thilo Gaul
  • Wolf Zimmermann
Conference paper
Part of the Advances in Computing Science book series (ACS)


In many cases, the effort of proving the correctness of large program systems seems not to be justifiable. Since heuristics and programming tricks are used and necessary to solve complex problems successfully, mathematical inductive argumentation often fails, because the algorithms to be verified get too complex and tricky. We need more modular approaches to guarantee program correctness.


Recursive Call Partial Correctness Register Allocation Program Verification Prototype Verification System 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Blum, M., Kannan, S. (1995). Designing programs that check their work. Journal of the ACM, 42 (1): 269–291.MATHCrossRefGoogle Scholar
  2. Boyer, R.S., Moore, J S. (1979): A Computational Logic. Academic Press Inc.Google Scholar
  3. Gaul, Th., Goos, G., Heberle, A., Zimmermann, W., Goerigk, W. (1997): An Architecture for Verified Compiler Construction. In: Proceedings Joint Modular Languages Conference 1997, Linz, AustriaGoogle Scholar
  4. Goerigk, W. (1996): An Exercise in Program Verification: The ACL2 Correctness Proof of a Simple Theorem Prover Executable. Techn. Report Verifix/CAU/2.4, CAU KielGoogle Scholar
  5. Goerigk, W., Dold, A., Gaul, Th., Goos, G., Heberle, A., von Henke, F.W., Hoffmann, U., Langmaack, H., Pfeifer, H., Rueß, H., Zimmermann, W. (1996): Compiler Correctness and Implementation Verification: The Verifix Approach. In: Proc. CC’96 Poster Session. IDA Technical Report LiTH-IDA-R-96–12, LinkøpingGoogle Scholar
  6. Goerigk, W., Hoffmann, U. (1996): The Compiler Implementation Language ComLisp. Technical Report Verifix/CAU/1.7, CAU KielGoogle Scholar
  7. Goerigk, W., Hoffmann, U. (1998): Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct. In: Proceedings of the International Workshop FMTrends’98, Lecture Notes in Computer Science, Springer Verlag. To AppearGoogle Scholar
  8. Goerigk, W., Müller-Olm, M. (1996): Erhaltung partieller Korrektheit bei beschränkten Maschinenressourcen. - Eine Beweisskizze -. Technical Report Verifix/CAU/2.5, CAU KielGoogle Scholar
  9. Goodenough, J.B., Gerhart, S.L. (1975): Toward a Theory of Test Data Selection. SIGPLAN Notices, 10 (6): 493–510CrossRefGoogle Scholar
  10. Heberle, A., Gaul, Th., Goerigk, W., Goos, G., Zimmermann, W. (1998): Construction of Verified Compiler Front Ends with Program-Checking. Submitted to CC’99 International Conference on Compiler ConstructionGoogle Scholar
  11. von Henke, F.W., Vialard, V., Dold, A., Goerigk, W. (1998): Admitting reflexive functions in PVS. Personal communication. UnpublishedGoogle Scholar
  12. Hoffmann, U. (1998): Compiler Implementation Verification through Rigorous Syntactical Code Inspection. PhD thesis. Technical Faculty of the Christian-AlbrechtsUniversity, KielGoogle Scholar
  13. Kaufmann, M., Moore, J S. (1994): Design Goals of ACL2. Technical Report 101, Computational Logic, Inc., Austin, TexasGoogle Scholar
  14. Lange, H., Möller, R., Neumann, B. (1996): Avoiding Combinatorial Explosion in Automatic Test Generation: Reasoning about Measurements is the Key. In: Proceedings of KI’96 Conference on Artificial Intelligence, Dresden. Springer VerlagGoogle Scholar
  15. Langmaack, H. (1997): Contribution to Goodenough’s and Gerhart’s Theory of Software Testing and Verification: Relation between Strong Compiler Test and Compiler Implementation Verification. In: C. Freksa, M. Jantzen, R. Valk (eds.): Foundations of Computer Science: Potential-Theory-Cognition. Lecture Notes in Computer Science 1337, Springer VerlagGoogle Scholar
  16. Moore, J S. (1996): Piton. A Mechanically Verified Assembly-Level Language. Kluver Academic Publishers, Dordrecht, Boston, LondonGoogle Scholar
  17. Moore, J S., Goerigk, W. (1998): Using checkers for admitting reflexive functions in ACL2. Personal communication. UnpublishedGoogle Scholar
  18. Müller-Olm, M. (1996): Three Views on Preservation of Partial Correctness. Technical Report Verifix/CAU/5.1. CAU KielGoogle Scholar
  19. Müller-Olm, M. (1997): Modular Compiler Verification. Lecture Notes in Computer Science 1283. Springer Verlag, Berlin, Heidelberg, New YorkGoogle Scholar
  20. Owre, S., Rushby, J.M., Shankar, N. (1992): PVS: A Prototype Verification System. In: Proceedings 11th International Conference on Automated Deduction CADE. Lecture Notes in Artificial Intelligence 607, pp. 748–752. Springer-VerlagGoogle Scholar
  21. Polak, W. (1981): Compiler Specification and Verification. In: G. Goos, J. Hartmanis (eds.) Lecture Notes in Computer Science 124. Springer-VerlagGoogle Scholar
  22. Wasserman, H., Blum, M. (1997). Software reliability via run-time result-checking. Journal of the ACM, 44 (6): 826–849.MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Wolfgang Goerigk
  • Thilo Gaul
  • Wolf Zimmermann

There are no affiliations available

Personalised recommendations