Abstract
We describe a software model checking tool founded on game semantics, highlight the underpinning theoretical results and discuss several case studies. The tool is based on an interpretation algorithm defined compositionally on syntax and thus can also handle open programs. Moreover, the models it produces are equationally fully abstract. These features are essential in the modeling and verification of software components such as modules and turn out to lead to very compact models of programs.
The authors gratefully acknowledge the support of UK EPSRC, Canadian NSERC and St. John’s College, Oxford University.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163 (2000)
Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I, II and III. Information and Computation 163 (2000)
Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In: Proc. of 1996 Workshop on Linear Logic. ENTCS, vol. 3, Elsevier, Amsterdam (1996); Also [22, Chap. 20]
Abramsky, S., McCusker, G.: Full abstraction for Idealized Algol with passive expressions. Theoretical Computer Science 227, 3–42 (1999)
Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Proc. of LICS 1998 (1998)
Laird, J.: Full abstraction for functional languages with control. In: Proc. of LICS 1997, pp. 58–67 (1997)
Hankin, C., Malacaria, P.: Generalised flowcharts and games. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 363. Springer, Heidelberg (1998)
Hankin, C., Malacaria, P.: Non-deterministic games and program analysis: an application to security. In: Proc. of LICS 1999, pp. 443–452 (1999)
Ghica, D.R., McCusker, G.: Reasoning about Idealized algol using regular languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 103. Springer, Heidelberg (2000)
Ghica, D.R.: Regular language semantics for a call-by-value programming language. In: 17th MFPS, Aarhus, Denmark. ENTCS, vol. 45, pp. 85–98. Elsevier, Amsterdam (2001)
Ghica, D.R.: A regular-language model for Hoare-style correctness statements. In: Proc. of the Verification and Computational Logic 2001, Florence, Italy (2001)
Ghica, D.R.: A Games-based Foundation for Compositional Software Model Checking. PhD thesis, Queen’s University School of Computing, Kingston, Ontario, Canada (2002)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Schmidt, D.A.: On the need for a popular formal semantics. ACM SIGPLAN Notices 32, 115–116 (1997)
Dill, D.L.: The Murφ verfication system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)
Holzmann, G.J., Peled, D.A.: The state of SPIN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 385–389. Springer, Heidelberg (1996)
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of 29th POPL, pp. 58–70. ACM Press, New York (2002)
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–275. Springer, Heidelberg (2001)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Zheng, H.: Bandera. In: Proc. of the 22nd International Conference on Software Engineering, pp. 439–448. ACM Press, New York (2000)
Reynolds, J.C.: The essence of Algol. In: de Bakker, J.W., van Vliet, J.C. (eds.) Algorithmic Languages, Proc. of the International Symposium on Algorithmic Languages, pp. 345–372. North-Holland, Amsterdam (1981)
O’Hearn, P.W., Tennent, R.D. (eds.): Algol-like Languages. Progress in Theoretical Computer Science, Two volumes. Birkhäuser, Boston (1997)
Abramsky, S.: Algorithmic game semantics: A tutorial introduction. Lecture notes, Marktoberdorf International Summer School 2001 (2001)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Reape, M., Thompson, H.S.: Parallel intersection and serial composition of finite state transducers. In: COLING 1988, pp. 535–539 (1988)
Ong, C.H.L.: Observational equivalence of third-order Idealized Algol is decidable. In: Proc. of LICS 2002, pp. 245–256 (2002)
Ghica, D.R., McCukser, G.: The regular-language semantics of first-order Idealized algol. Theoretical Computer Science (to appear)
Murawski, A.S.: Variable scope and call-by-value program equivalence (2003) (in preparation)
Senizergues: L(A) = L(B)? decidability results from complete formal systems. TCS: Theoretical Computer Science 251 (2001)
Stirling, C.: Deciding DPDA equivalence is primitive recursive. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 821–865. Springer, Heidelberg (2002)
Murawski, A.S.: On program equivalence in languages with ground-type references. In: Proc. of LICS 2003, IEEE Computer Society Press, Los Alamitos (2003)
Murawski, A.S.: Complexity of first-order call-by-name program equivalence (2003) (submitted for publication)
AT&T FSM Librarytm – general-purpose finite-state machine software tools, http://www.research.att.com/sw/tools/fsm/
Ghica, D.R.: Game-based software model checking: Case studies and methodological considerations. Technical Report PRG-RR-03-11, Oxford University Computing Laboratory (2003)
Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher-Order and Symbolic Computation 13, 315–353 (2000)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Dwork, C. (ed.) Proc. of the 9th Annual ACM Symposium on Principles of Distributed Computing, Québec City, Québec, Canada, pp. 377–408. ACM Press, New York (1990)
Colby, C., Godefroid, P., Jagadeesan, L.: Automatically closing open reactive programs. In: Proc. of PLDI 1998, Montreal, Canada, pp. 345–357 (1998)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Gruhn, V. (ed.) Proc. of the 9th ESEC/FSE 2001. Software Engineering Notes, vol. 26(5), pp. 109–120. ACM Press, New York (2001)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. of the ACM 49, 672–713 (2002)
Ghica, D.R., Murawski, A.S.: Angelic semantics of fine-grained concurrency. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 211–225. Springer, Heidelberg (2004) (to appear)
Lazic, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, University of Oxford (1999)
Lazic, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 581. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.H.L. (2004). Applying Game Semantics to Compositional Software Modeling and Verification. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive