Skip to main content
SpringerLink
Log in
Book cover

Technologie, Wachstum und Beschäftigung pp 256–263Cite as

Programmverifikation und Künstliche Intelligenz

  • Chapter

  • 184 Accesses

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.

This is a preview of subscription content, 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   59.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   79.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literatur

  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 York

    Google Scholar 

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

    Google Scholar 

  3. Boyer R S, Moore J S (1975) Proving theorems about LISP functions. JACM 22:129–144

    Article  Google Scholar 

  4. Dreyfus H L, Dreyfus S E (1986) Mind over machine. The free press. New York

    Google Scholar 

  5. Ehrig H., Kreowski H J, Mahr B, Padawitz (1982) Algebraic implementation of abstract data types. TCS 20:209–263

    Article  Google Scholar 

  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 6487

    Google Scholar 

  7. Gordon M, Milner R, Wadsworth C (1979) Edinburgh-LCF. LNCS 78 Springer-Verlag Berlin Heidelberg New York

    Google Scholar 

  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 York

    Google Scholar 

  9. Harel D (1979) First-Order Dynamic Logic. LNCS 68. Springer-Verlag Berlin Heidelberg New York

    Google Scholar 

  10. Hoare CAR (1969) An axiomatic basis for computer programming. Communications of the ACM 12:576–580

    Article  Google Scholar 

  11. Igarashi S, London R, Luckham C (1975) Automatic program verification. Acta Informatica 4:145–182

    Article  Google Scholar 

  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 York

    Google Scholar 

  13. Newell A, Shaw J C, Simon H (1959) Report on a general problem solving program. Proc. Int. Conf. Information Processing. Paris

    Google Scholar 

  14. Pnueli A (1977) The temporal logic of programs. Proc. 18th I.E. E. E. Annual Symposium on Foundations of Computer Science. Providence

    Google Scholar 

  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 York

    Google Scholar 

  16. Thomas Ch (1984) RR Lab-Ein Labor für Termersetzungssysteme. MEMO-SEKI-84–1. FBI Universität Kaiserslautern

    Google Scholar 

Download references

Authors
  1. Wolfram Menzel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Werner Stephan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Statistik und Mathematische Wirtschaftstheorie Rechenzentrum, Universität Karlsruhe, Zirkel 2, Postfach 6980, 7500, Karlsruhe 1, Germany

    Rudolf Henn

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Menzel, W., Stephan, W. (1987). Programmverifikation und Künstliche Intelligenz. In: Henn, R. (eds) Technologie, Wachstum und Beschäftigung. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-72831-0_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-72831-0_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-72832-7

  • Online ISBN: 978-3-642-72831-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation