Program Verification by Symbolic Execution and Induction | SpringerLink
Skip to main content
Springer Nature Link
Log in

Program Verification by Symbolic Execution and Induction

  • Conference paper
GWAI-87 11th German Workshop on Artifical Intelligence

Part of the book series: Informatik-Fachberichte ((2252,volume 152))

Abstract

BURSTALL’s verification method which is based on symbolic execution and mathematical induction is extended and formalized within the framework of dynamic logic. An example is presented. An implementation using the metalanguage of the Karlsruhe Interactive Verifier is described.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

  1. Boyer, R.S./ Moore, J.S. A Computational Logic. Academic Press, New York 1979

    Google Scholar 

  2. Burstall, R.M. Program Proving as Hand Simulation with a little Induction. Information Processing 74, North-Holland Publishing Company (1974)

    Google Scholar 

  3. Constable,R./Knoblock,T./Bates,J. Writing Programs That Construct Proofs. Journal of Automated Reasoning, Vol. 1, No. 3, pp 285 - 326 (1985)

    MathSciNet  Google Scholar 

  4. Gordon,M/Milner,R./Wadsworth,C. Edinburgh LCF. Springer LNCS 78 (1979)

    Google Scholar 

  5. Harel, D. Dynamic Logic. Handbook of Philosophical Logic, D. Gabbay and F. Guenther (eds.), Reidel (1984), Vol. 2, 496 - 604

    Google Scholar 

  6. Hähnle, R./Heisel, M./Reif, W./Stephan, W. An Interactive Verification System Based on Dynamic Logic. Proc. 8-th International Conference on Automated Deduction, J.Siekmann (ed), Springer LNCS 230 (1986), 306 - 315

    Google Scholar 

  7. Heisel,M./.Reif, W./Stephan, W. A Functional Language to Construct Proofs. Interner Bericht 1/86, Fakultät für Informatik, Universität Karlsruhe (1986)

    Google Scholar 

  8. Horowitz,E./Sahni,S. Data Structures in Pascal. Computer Science Press (1987)

    Google Scholar 

  9. Reif, W., Vollständigkeit einer modifizierten Goldblatt-Logik und Approximation der Omegaregel durch Induktion. Diplomarbeit, Fakultät für Informatik, Universität Karlsruhe (1984)

    Google Scholar 

  10. Richter, M.M. Logikkalküle, Teubner (1978)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Postfach 6980, D-7500, Karlsruhe, Germany

    M. Heisel, W. Reif & W. Stephan

Authors
  1. M. Heisel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. W. Reif
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. W. Stephan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Projektgruppe KIT, Sekr. FR 5–8, Technische Universität Berlin, Franklinstraße 28/29, D-1000, Berlin 10, Deutschland

    Katharina Morik

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heisel, M., Reif, W., Stephan, W. (1987). Program Verification by Symbolic Execution and Induction. In: Morik, K. (eds) GWAI-87 11th German Workshop on Artifical Intelligence. Informatik-Fachberichte, vol 152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-73005-4_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-73005-4_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-18388-4

  • Online ISBN: 978-3-642-73005-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation