Assume-Guarantee Software Verification Based on Game Semantics

  • Aleksandar Dimovski
  • Ranko Lazić
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


We show how game semantics, counterexample-guided abstraction refinement, assume-guarantee reasoning and the L * algorithm for learning regular languages can be combined to yield a procedure for compositional verification of safety properties of open programs. Game semantics is used to construct accurate models of subprograms compositionally. Overall model construction is avoided using assume-guarantee reasoning and the L * algorithm, by learning assumptions for arbitrary subprograms. The procedure has been implemented, and initial experimental results show significant space savings.


Model Check Regular Language Safety Property Membership Query Observation Table 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    Abramsky, S., Jagadeesan, R., Malacaria, P.: Full Abstraction for PCF. Information and Computation 163(2) (2000)Google Scholar
  3. 3.
    Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algol-like languages. Birkhaüser, Basel (1997)Google Scholar
  4. 4.
    Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation 75(2), 87–106 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Chaki, S., Clarke, E., Sharygina, N., Sinha, N.: Dynamic Component Substiutability Analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 512–528. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  9. 9.
    Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Dimovski, A., Lazic, R.: CSP Representation of Game Semantics for Second-Order Idealized Algol. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 146–161. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    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
  12. 12.
    Dimovski, A., Ghica, D.R., Lazic, R.: A Counterexample-Guided Refinement Tool for Open Procedural Programs. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 288–292. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Formal Systems (Europe) Ltd Failures-Divergence Refinement: FDR2 Manual (2000),
  14. 14.
    Ghica, D.R., McCusker, G.: The Regular-Language Semantics of Second-order Idealized Algol. Theoretical Computer Science 309(1–3), 469–502 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Groce, A., Peled, D., Yannakakis, M.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Harmer, R.: Games and Full Abstraction for Nondeterministic Languages. PhD thesis, Imperial College (1999)Google Scholar
  17. 17.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Hyland, J.M.E., Ong, C.-H.L.: On Full Abstraction for PCF: I, II, and III. Information and Computation 163, 285–400 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Laird, J.: A Fully Abstract Game Semantics of Local Exceptions. In: Proceedings of LICS, pp. 105–114 (2001)Google Scholar
  20. 20.
    Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. Logic and Models of Concurrent Systems 13, 123–144 (1984)Google Scholar
  21. 21.
    Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Aleksandar Dimovski
    • 1
  • Ranko Lazić
    • 1
  1. 1.Department of Computer ScienceUniversity of WarwickCoventryUK

Personalised recommendations