On-the-Fly Techniques for Game-Based Software Model Checking

  • Adam Bakewell
  • Dan R. Ghica
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.


Model Check Game Model Data Approximation Abstract Interpretation Automaton Tree 
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.


  1. 1.
    Abramsky, S.: Abstract interpretation, logical relations and kan extensions. J. Log. Comput. 1(1), 5–40 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Bakewell, A., Ghica, D.R.: Game-Based Safety Checking with Mage. In: SAVCBS, pp. 85–87 (2007)Google Scholar
  5. 5.
    Bakewell, A., and Ghica, D. R. On-the-Fly Techniques for Game-Based Software Model Checking (extended report). Technical Report TR-07-8, School of Computer Science, University of Birmingham (2007)Google Scholar
  6. 6.
    Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)Google Scholar
  7. 7.
    Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of c programs. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 203–213 (2001)Google Scholar
  8. 8.
    Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  11. 11.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)Google Scholar
  12. 12.
    Cousot, P., Cousot, R.: Higher-order abstract interpretation, invited paper. In: Proc. 1994 International Conference on Computer Languages, pp. 95–112. IEEE Computer Society Press, Los Alamitos (1994)CrossRefGoogle Scholar
  13. 13.
    Dimovski, A., Ghica, D.R., Lazic, R.: Data-abstraction refinement: A game semantic approach. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 102–117. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Ghica, D.R., Lazić, R.S., Dimovski, A.: A counterexample-guided refinement tool for open procedural programs. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 288–292. Springer, Heidelberg (2006)Google Scholar
  15. 15.
    Ghica, D.R., McCusker, G.: The regular-language semantics of second-order idealized Algol. Theor. Comput. Sci. 309(1-3), 1–3 (2003)CrossRefMathSciNetGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Henzinger, T., Jhala, R., Majumdar, R., Sanvido, M.: Extreme model checking (2003)Google Scholar
  18. 18.
    Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast (2003)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  22. 22.
    Laird, J.: A fully abstract game semantics of local exceptions. In: LICS, pp. 105–114 (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Adam Bakewell
    • 1
  • Dan R. Ghica
    • 1
  1. 1.University of BirminghamUK

Personalised recommendations