Article

Compositional Predicate Abstraction from Game Semantics

Authors:

Dan R. GhicaAuthors Info & Claims

TACAS '09: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,

Pages 62 - 76

https://doi.org/10.1007/978-3-642-00768-2_8

Published: 27 March 2009 Publication History

Abstract

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 <Emphasis Type="SmallCaps">Mage</Emphasis>, and we illustrate it with several toy examples.

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).

[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).

[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).

[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).

[7]

Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409-470 (2000).

[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).

[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).

[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).

[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).

[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).

[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.

[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).

[18]

Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55-74 (2002).

Cited By

Dimovski A(2018)Verifying annotated program families using symbolic game semanticsTheoretical Computer Science10.1016/j.tcs.2017.09.029706:C(35-53)Online publication date: 6-Jan-2018
https://dl.acm.org/doi/10.1016/j.tcs.2017.09.029
Dimovski A(2014)Program verification using symbolic game semanticsTheoretical Computer Science10.1016/j.tcs.2014.01.016560:P3(364-379)Online publication date: 4-Dec-2014
https://dl.acm.org/doi/10.1016/j.tcs.2014.01.016
Hopkins DMurawski AOng C(2012)HECTORProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_63(774-780)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_63
Show More Cited By

Compositional Predicate Abstraction from Game Semantics
1. Theory of computation

Recommendations

Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Ranked predicate abstraction for branching time: complete, incremental, and precise
ATVA'06: Proceedings of the 4th international conference on Automated Technology for Verification and Analysis

Predicate abstraction frameworks are a powerful means of combating the state explosion problem in model checking as they automatically synthesize abstract models that either verify compliance with a property, give rise to a genuine counter-example or ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS '09: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,

March 2009

453 pages

ISBN:9783642007675

Editors:
Stefan Kowalewski
Embedded Software Laboratory, RWTH Aachen, Aachen, Germany 52074
,
Anna Philippou
Department of Computer Science, University of Cyprus, Nicosia, CY-1678, Cyprus

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 March 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dimovski A(2018)Verifying annotated program families using symbolic game semanticsTheoretical Computer Science10.1016/j.tcs.2017.09.029706:C(35-53)Online publication date: 6-Jan-2018
https://dl.acm.org/doi/10.1016/j.tcs.2017.09.029
Dimovski A(2014)Program verification using symbolic game semanticsTheoretical Computer Science10.1016/j.tcs.2014.01.016560:P3(364-379)Online publication date: 4-Dec-2014
https://dl.acm.org/doi/10.1016/j.tcs.2014.01.016
Hopkins DMurawski AOng C(2012)HECTORProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_63(774-780)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_63
Kobayashi NSato RUnno HHall MPadua D(2011)Predicate abstraction and CEGAR for higher-order model checkingProceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1993498.1993525(222-233)Online publication date: 4-Jun-2011
https://dl.acm.org/doi/10.1145/1993498.1993525
Kobayashi NSato RUnno H(2011)Predicate abstraction and CEGAR for higher-order model checkingACM SIGPLAN Notices10.1145/1993316.199352546:6(222-233)Online publication date: 4-Jun-2011
https://dl.acm.org/doi/10.1145/1993316.1993525

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents