Skip to main content
SpringerLink
Log in

Model Checking Algol-Like Languages Using Game Semantics

  • Conference paper
  • First Online:
FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002)

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

  • 501 Accesses

Abstract

We survey a recent development of Game Semantics in a new, algorithmic direction, with a view to applications in computer-assisted verification and program analysis.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky, K. Honda, and G. McCusker. Fully abstract game semantics for general reference. In Proceedings of IEEE Symposium on Logic in Computer Science, 1998. Computer Society Press, 1998.

    Google Scholar 

  2. S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163, 2000.

    Google Scholar 

  3. S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In P. W. O’Hearn and R. D. Tennent, editors, Algol-like languages. Birkhaüser, 1997.

    Google Scholar 

  4. E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  5. V. Danos and R. Harmer. Probabilistic game semantics. In Proc. IEEE Symposium on Logic in Computer Science, Santa Barbara, June, 2000. Computer Science Society, 2000.

    Google Scholar 

  6. D. R. Ghica and G. McCusker. Reasoning about Idealized Algol using regular languages. In Proceedings of 27th International Colloquium on Automata, Languages and Programming ICALP 2000, pages 103–116. Springer-Verlag, 2000. LNCS Vol. 1853.

    Chapter  Google Scholar 

  7. S. Ginsberg and S. Greibach. Deterministic context-free languages. Information and Control, pages 620–648, 1966.

    Google Scholar 

  8. R. Harmer and G. McCusker. A fully abstract game semantics for finite nondeterminism. In Proceedings of Fourteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999.

    Google Scholar 

  9. D. H. D. Hughes. Games and definability for System F. In Proceedings of 12th IEEE Symposium on Logic in Computer Science. IEEE Computer Science Society, 1997.

    Google Scholar 

  10. J. M. E. Hyland and C.-H. L. Ong. On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Information and Computation, 163:285–408, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  11. A. D. Ker, H. Nickau, and C.-H. L. Ong. A universal innocent game model for the Böhm tree lambda theory. In Computer Science Logic: Proceedings of the 8th Annual Conference on the EACSL Madrid, Spain, September 1999, pages 405–419. Springer-Verlag, 1999. LNCS Volume 1683.

    Chapter  Google Scholar 

  12. A. D. Ker, H. Nickau, and C.-H. L. Ong. Innocent game models of untyped λ-calculus. Theoretical Computer Science, 272:247–292, 2002.

    Article  MATH  MathSciNet  Google Scholar 

  13. J. Laird. A semantic analysis of control. PhD thesis, University of Edinburgh, 1998.

    Google Scholar 

  14. A. Murawski. Finitary higher-order programming languages with first-order references are undecidable. Preprint, 2002.

    Google Scholar 

  15. C.-H. L. Ong. Observational equivalence of third-order Idealized Algol is decidable. In Proceedings of IEEE Symposium on Logic in Computer Science, 22–25 July 2000, Copenhagen Denmark, pages 245–256. Computer Society Press, 2002.

    Google Scholar 

  16. J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372. North Holland, 1978.

    Google Scholar 

  17. D. A. Schmidt. On the need for a popular formal semantics. ACM SIGPLAN Notices, 32:115–116, 1997.

    Article  MATH  Google Scholar 

  18. G. Sénizergues. L(A) = L(B)? Decidability results from complete formal systems. Theoretical Computer Science, 251:1–166, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  19. C. Stirling. Decidability of DPDA equivalence. Theoretical Computer Science, 255:1–31, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  20. M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Banff Higher Order Workshop, pages 238–266. Springer-Verlag, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    C. -H. L. Ong

  2. School of Computing, National University of Singapore, Singapore

    C. -H. L. Ong

Authors
  1. C. -H. L. Ong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, 208016, Kanpur, India

    Manindra Agrawal  & Anil Seth  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ong, C.H.L. (2002). Model Checking Algol-Like Languages Using Game Semantics. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

  • Online ISBN: 978-3-540-36206-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation