Skip to main content

Tutorial: Proving properties of concurrent systems with SPIN

  • Invited Papers
  • Conference paper
  • First Online:

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

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

References

  1. J. Chaves, ‘Formal methods at AT&T, an industrial usage report,’ Proc. 4th FORTE Conference, Sydney, Australia, 1991, pp. 83–90.

    Google Scholar 

  2. Y. Choueka. “Theories of automata on ω-tapes: a simplified approach.’ Journal of Computer and System Science. Vol. 8, 1974, pp. 117–141.

    Google Scholar 

  3. G. Bhat, R. Cleaveland, and O. Grumberg. ‘Efficient on-the-fly model checking for CTL*.’ Proc. 10th Symp. on Logic in Computer Science, San Diego, CA, 1995.

    Google Scholar 

  4. C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, ‘Memory efficient algorithms for the verification of temporal properties.’ Formal Methods in Systems Design, Vol I. 1992, pp. 275–288.

    Article  Google Scholar 

  5. R. Gerth, D. Peled, M. Y. Vardi, P. Wolper, 'simple on-the-fly automatic verification of linear temporal logic,’ Proc. IFIP/WG6.1 Symp. on Protocol Specification, Testing, and Verification, PSTV95, Warsaw, Poland, June 1995.

    Google Scholar 

  6. G. J. Holzmann, ‘An unproved protocol reachability analysis technique,’ Software, Practice and Experience, 18(2): 137–161, 1988.

    Google Scholar 

  7. P. Godefroid and G. J. Holzmann, ‘On the verification of temporal properties,’ Proc. IFIP/WG6.1 Symp. on Protocol Specification. Testing, and Verification, PSTV93, Liege, Belgium, June 1993.

    Google Scholar 

  8. G. J. Holzmann, Design and validation of computer protocols. Prentice Hall. Englewood Cliffs, NJ, 1991.

    Google Scholar 

  9. G. J. Holzmann, ‘The theory and practice of a formal method: NewCoRe,’ Proc. 13th IFIP World Computer Congress, Hamburg. Germany, 1994, pp. 35–44.

    Google Scholar 

  10. G. J. Holzmann and D. Peled, ‘An improvement in formal verification,’ Proc. 7th FORTE Conference, Bern, Switzerland, 1994.

    Google Scholar 

  11. G. J. Holzmann. ‘An analysis of bitstate hashing,’ Proc. IFIP/WG6.1 Symp. on Protocol Specification. Testing, and Verification, PSTV95, Warsaw, Poland, June 1995.

    Google Scholar 

  12. R. E. Tarjan. ‘Depth first search and linear graph algorithms.’ SIAM J. Computing. 1:2, pp. 146–160, 1972.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Insup Lee Scott A. Smolka

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Holzmann, G.J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_34

Download citation

  • DOI: https://doi.org/10.1007/3-540-60218-6_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60218-7

  • Online ISBN: 978-3-540-44738-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics