Skip to main content
SpringerLink
Log in

Deductive verification of invariants of state-transition systems

  • Technical Papers-section 3
  • Conference paper
  • First Online:
KI-98: Advances in Artificial Intelligence (KI 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1504))

Included in the following conference series:

  • 205 Accesses

Abstract

We present a modular technique to prove invariants of statetransition systems in a deductive framework. We show how the semantic knowledge of the given problem can be generically used to decompose the problem into modular tasks which can be successfully tackled with the help of techniques developed in the field of inductive theorem proving. As an example we present the mechanical verification of the invariant of a case study specifying a generic elevator.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. N.S. Bjørner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H.B. Sipma, T.E. Uribe: STeP: Deductive-algorithmic verification of reactive and real-time systems. 8th Computer Aided Verification CAV, Springer, LNCS 1102, 1996

    Google Scholar 

  2. A. Browne, Z. Manna, H.B. Sipma: Generalized temporal verification diagrams. 15th Conference on Foundations of Software Technology and Theoretical Computer Science, Springer, LNCS 1026, 1995

    Google Scholar 

  3. A. Bundy, A. Stevens, F. v. Harmelen, A. Ireland, and A. Smaill: Rippling: a heuristic for guiding inductive proofs. Journal of Artificial Intelligence, pp. 185–253, No. 62, 1993

    Article  MATH  Google Scholar 

  4. D. Hutter, C. Sengler: INKA—The Next Generation 13th Int. Conference on Automated Deduction CADE, Springer, LNAI 1104, 1996

    Google Scholar 

  5. D. Hutter: Colouring Terms to Control Equational Reasoning. Journal of Automated Reasoning, Vol. 18, pp. 399–442, 1997

    Article  MATH  MathSciNet  Google Scholar 

  6. Z. Manna, A. Pnueli: Temporal verification diagrams Int. Symp. on Theoretical Aspects of Computer Software, Springer, LNCS 789, 1994

    Google Scholar 

  7. Z. Manna, A. Pnueli: Temporal Verification of Reactive Systems: Safety. Springer, New York, 1995

    Google Scholar 

  8. N. Shankar: Verification of real time systems using PVS 5th Computer Aided Verification CAV, Springer, LNCS 697, 1993

    Google Scholar 

  9. D. Hutter, B. Langenstein, C. Sengler, J. Siekmann, W. Stephan, and A. Wolpers: Deduction in the Verification Support Environment (VSE). Formal Methods Europe 96, Oxford, Great Britain, 1996

    Google Scholar 

  10. C. Walther: Mathematical Induction. Handbook of Logic in AI and Logic Programming, Vol. 2, Oxford Press, 1994

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. German Research Center for Artificial Intelligence GmbH, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter

Authors
  1. Dieter Hutter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Otthein Herzog Andreas Günter

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hutter, D. (1998). Deductive verification of invariants of state-transition systems. In: Herzog, O., Günter, A. (eds) KI-98: Advances in Artificial Intelligence. KI 1998. Lecture Notes in Computer Science, vol 1504. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0095436

Download citation

  • DOI: https://doi.org/10.1007/BFb0095436

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65080-5

  • Online ISBN: 978-3-540-49656-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation