×

zbMATH — the first resource for mathematics

Compositional predicate abstraction from game semantics. (English) Zbl 1234.68069
Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 62-76 (2009).
Summary: We introduce a technique for using conventional predicate abstraction methods to reduce the state-space of models produced using game semantics. We focus on an expressive procedural language that has both local store and local control, a language which enjoys a simple game-semantic model yet is expressive enough to allow non-trivial examples. Our compositional approach allows the verification of incomplete programs (e.g. libraries) and offers the opportunity for new heuristics for improved efficiency. Game-semantic predicate abstraction can be embedded in an abstraction-refinement cycle in a standard way, resulting in an improved version of our experimental model-checking tool Mage, and we illustrate it with several toy examples.
For the entire collection see [Zbl 1157.68007].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
91A80 Applications of game theory
Software:
BLAST
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Slam and static driver verifier: Technology transfer of formal methods inside Microsoft. In: IFM, pp. 1–20 (2004)
[2] Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST software verification system. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 25–26. Springer, Heidelberg (2005)
[3] Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.-H.L.: Applying game semantics to compositional software modeling and verification. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 421–435. Springer, Heidelberg (2004) · Zbl 1126.68343
[4] Dimovski, A., Ghica, D.R., Lazić, R.S.: Data-abstraction refinement: A game semantic approach. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 102–117. Springer, Heidelberg (2005) · Zbl 1141.68366
[5] Ghica, D.R., Murawski, A.S.: Compositional model extraction for higher-order concurrent programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 303–317. Springer, Heidelberg (2006) · Zbl 1180.68115
[6] Bakewell, A., Ghica, D.R.: On-the-fly techniques for game-based software model checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 78–92. Springer, Heidelberg (2008) · Zbl 1134.68396
[7] Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000) · Zbl 1006.68028
[8] Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000) · Zbl 1006.68027
[9] Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999) · Zbl 1046.68589
[10] Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. Electr. Notes Theor. Comput. Sci. 3 (1996) · Zbl 0909.68029
[11] Laird, J.: A fully abstract game semantics of local exceptions. In: LICS, pp. 105–114 (2001)
[12] Reynolds, J.: The craft of programming. Prentice-Hall, Englewood Cliffs (1981) · Zbl 0476.68010
[13] Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algol-Like Languages, July 1996, vol. 2, pp. 173–193. Birkhauser, Basel (1997); reprinted from Proceedings Eleventh Annual IEEE Symposium on Logic in Computer Science, Brunswick, NJ, July 1996, pp. 152–163 (2006)
[14] Ghica, D.R., McCusker, G.: The regular-language semantics of second-order Idealized Algol. Theor. Comput. Sci. 309(1-3), 469–502 (2003) · Zbl 1070.68083
[15] Ong, C.H.L.: Observational equivalence of 3rd-order Idealized Algol is decidable. In: LICS, pp. 245–256 (2002)
[16] Laird, J.: A game semantics of names and pointers. Annals of Pure and Applied Logic 151(2-3), 151–169 (2008); first Games for Logic and Programming Languages Workshop · Zbl 1133.68014
[17] Chaki, S., Clarke, E., Groce, A., Strichman, O.: Predicate abstraction with minimum predicates. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 19–34. Springer, Heidelberg (2003) · Zbl 1179.68033
[18] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.