Skip to main content
SpringerLink
Log in

Formalization of variables access constraints to support compositionality of liveness properties

  • Conference paper
  • First Online:
Higher Order Logic Theorem Proving and Its Applications (HUG 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 780))

Included in the following conference series:

Abstract

Because reasoning about programs' liveness behavior is difficult people become interested in the potential of theorem provers to aid verification. In extending a theorem prover with a lifeness logic it would be nice if compositionality is also supported since it is a property of a great practical interest: it allows modularity in design. However, a straightforward extension that only embodies the essence of the logic will fail to do so. In implementing such an extension we should therefore be aware of the technical details required for compositionality. In particular, compositionality of progress under parallel composition depends on the concept of variable accessibility. Therefore, this concept has to be explicitly present in the extension. This paper is about the formalization of access constraints to support compositionality.

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. Flemming Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, 1992.

    Google Scholar 

  2. Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the hol theorem prove. Technical Report 265, University of Cambridge, 1992.

    Google Scholar 

  3. K.M. Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley Publishing Company, Inc., 1988.

    Google Scholar 

  4. Mike JC Gordon and Tom F Melham. Introduction to HOL. Cambridge University Press, 1993.

    Google Scholar 

  5. Roger W.S. Hale. Programming in Temporal Logic. PhD thesis, University of Cambridge, 1988.

    Google Scholar 

  6. J. Pachl. Three definitions of leads-to for UNITY. Notes on UNITY, 23–90, December 1990.

    Google Scholar 

  7. ISWB Prasetya. Documentation of HOL-Library UNITY. University of Utrecht, 1993. Will appear as a technical report.

    Google Scholar 

  8. A.K. Singh. Leads-to and program union. Notes on UNITY, 06–89, 1989.

    Google Scholar 

  9. J. von Wright and T. Långbacka. Using a theorem prover for reasoning about concurent algorithms. In Proc. 4th Workshop on Computer-Aided Verification, Montreal, Canada, June 1992. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Vakgroep Informatica, Rijksuniversiteit Utrecht, Postbus 80.089, 3508, TB Utrecht, Nederland

    Iswb Prasetya

Authors
  1. Iswb Prasetya
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jeffrey J. Joyce Carl-Johan H. Seger

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Prasetya, I. (1994). Formalization of variables access constraints to support compositionality of liveness properties. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_145

Download citation

  • DOI: https://doi.org/10.1007/3-540-57826-9_145

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57826-0

  • Online ISBN: 978-3-540-48346-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation