Advertisement

Programmverifikation und Künstliche Intelligenz

  • Wolfram Menzel
  • Werner Stephan
Chapter

Zusammenfassung

Ein großes Programmsystem, das heute zum ersten Mal die Hand seiner Programmierer verläßt, arbeitet kaum je fehlerfrei. Es gibt aber Situationen, in denen man auf völliger Korrektheit bestehen muß. Formale Programmverifikation ist auf die Dauer unentbehrlich. In ihrer heutigen Gestalt beinhaltet sie eine Gesamtdisziplin des formalen Vorgehens bei der Programmerstellung, und sie bedient sich der zentralen und weitest fortgeschrittenen Techniken der Künstlichen Intelligenz.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literatur

  1. 1.
    Biundo S, Hummel B, Hutter D, Walther C (1986) The Karlsruhe induction proving system. Proc. 8th International Conference on Automated Deduction, Oxford. LNCS 230. Springer-Verlag Berlin Heidelberg New YorkGoogle Scholar
  2. 2.
    Bläsius K, Eisinger N, Herold A, Siekmann J, Smolka G, Walther C (1981) The Markgraf Karl refutation Procedure. Proc. of the 7th International Joint Conference on Artificial Intelligence. VancouverGoogle Scholar
  3. 3.
    Boyer R S, Moore J S (1975) Proving theorems about LISP functions. JACM 22:129–144CrossRefGoogle Scholar
  4. 4.
    Dreyfus H L, Dreyfus S E (1986) Mind over machine. The free press. New YorkGoogle Scholar
  5. 5.
    Ehrig H., Kreowski H J, Mahr B, Padawitz (1982) Algebraic implementation of abstract data types. TCS 20:209–263CrossRefGoogle Scholar
  6. 6.
    Goguen J A, Thatcher J W, Wagner E G (1976) An initial algebra approach to the specification, correctness, and implementation of abstract data types. IBM Research Report RC 6487Google Scholar
  7. 7.
    Gordon M, Milner R, Wadsworth C (1979) Edinburgh-LCF. LNCS 78 Springer-Verlag Berlin Heidelberg New YorkGoogle Scholar
  8. 8.
    Hähnle R, Heisel M, Reif W, Stephan W (1986) An interactive verification system based on dynamic logic. Proc. 8th International Conference on Automated Deduction, Oxford. LNCS 230. Springer-Verlag Berlin Heidelberg New YorkGoogle Scholar
  9. 9.
    Harel D (1979) First-Order Dynamic Logic. LNCS 68. Springer-Verlag Berlin Heidelberg New YorkGoogle Scholar
  10. 10.
    Hoare CAR (1969) An axiomatic basis for computer programming. Communications of the ACM 12:576–580CrossRefGoogle Scholar
  11. 11.
    Igarashi S, London R, Luckham C (1975) Automatic program verification. Acta Informatica 4:145–182CrossRefGoogle Scholar
  12. 12.
    Käufl Th (1986) Programm verifier, Tatzelwurm’: Reasoning about systems of linear inequalities. Proc. 8th International Conference on Automated Deduction, Oxford. LNCS 230. Springer-Verlag Berlin Heidelberg New YorkGoogle Scholar
  13. 13.
    Newell A, Shaw J C, Simon H (1959) Report on a general problem solving program. Proc. Int. Conf. Information Processing. ParisGoogle Scholar
  14. 14.
    Pnueli A (1977) The temporal logic of programs. Proc. 18th I.E. E. E. Annual Symposium on Foundations of Computer Science. ProvidenceGoogle Scholar
  15. 15.
    Stickel M E (1986) A PROLOG technology theorem pro ver implementation by an extended PROLOG compiler. Proc. 8th International Conference on Automated Deduction, Oxford. LNCS 230. SpringerVerlag Berlin Heidelberg New YorkGoogle Scholar
  16. 16.
    Thomas Ch (1984) RR Lab-Ein Labor für Termersetzungssysteme. MEMO-SEKI-84–1. FBI Universität KaiserslauternGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1987

Authors and Affiliations

  • Wolfram Menzel
  • Werner Stephan

There are no affiliations available

Personalised recommendations