Skip to main content
SpringerLink
Log in

Using Graph Transformations and Graph Abstractions for Software Verification

  • Conference paper
Graph Transformations (ICGT 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6372))

Included in the following conference series:

Abstract

In this abstract we present an overview of our intended approach for the verification of software written in imperative programming languages. This approach is based on model checking of graph transition systems (GTS), where each program state is modeled as a graph and the exploration engine is specified by graph transformation rules. We believe that graph transformation [13] is a very suitable technique to model the execution semantics of languages with dynamic memory allocation. Furthermore, such representation provides a clean setting to investigate the use of graph abstractions, which can mitigate the space state explosion problem that is inherent to model checking techniques.

The work reported herein is being carried out as part of the GRAIL project, funded by NWO (Grant 612.000.632).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Baldan, P., König, B., König, B.: A logic for analyzing abstractions of graph transformation systems. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 255–272. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  2. Bauer, J., Boneva, I.B., Kurban, M.E., Rensink, A.: A modal-logic based graph abstraction. In: Ehrig, et al. (eds.) [4], pp. 321–335

    Google Scholar 

  3. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238–252 (1977)

    Google Scholar 

  4. Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.): ICGT 2008. LNCS, vol. 5214. Springer, Heidelberg (2008)

    Google Scholar 

  5. Kastenberg, H., Kleppe, A., Rensink, A.: Defining object-oriented execution semantics using graph transformations. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 186–201. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. König, B., Kozioura, V.: Augur – a new version of a tool for the analysis of graph transformation systems. ENTCS 211, 201–210 (2008)

    Google Scholar 

  8. Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Rensink, A., Zambon, E.: A type graph model for Java programs. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 237–242. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Rensink, A.: The GROOVE simulator: A tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)

    Google Scholar 

  11. Rensink, A., Distefano, D.: Abstract graph transformation. Electr. Notes Theor. Comput. Sci. 157(1), 39–59 (2006)

    Article  Google Scholar 

  12. Rieger, S., Noll, T.: Abstracting complex data structures by hyperedge replacement. In: Ehrig, et al. (eds.) [4], pp. 69–83

    Google Scholar 

  13. Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations. Foundations, vol. 1. World Scientific, Singapore (1997)

    MATH  Google Scholar 

  14. Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

    Article  Google Scholar 

  15. Smelik, R., Rensink, A., Kastenberg, H.: Specification and construction of control flow semantics. In: Visual Languages and Human-Centric Computing (VL/HCC), Brighton, UK, pp. 65–72. IEEE Computer Society Press, Los Alamitos (September 2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods and Tools Group, University of Twente, The Netherlands

    Eduardo Zambon

Authors
  1. Eduardo Zambon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin, Franklinstr. 28/29, 10587, Berlin, Germany

    Hartmut Ehrig

  2. Afdeling Informatica, Universiteit Twente, Drienerlolaan 5, 7522, Enschede, NB, The Netherlands

    Arend Rensink

  3. Leiden Institute of Advanced Computer Science (LIACS), Universiteit Leiden, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

  4. Fachgebiet Echtzeitsysteme, Technische Universität Darmstadt, Merckstraße 25, 64283, Darmstadt, Germany

    Andy Schürr

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zambon, E. (2010). Using Graph Transformations and Graph Abstractions for Software Verification. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds) Graph Transformations. ICGT 2010. Lecture Notes in Computer Science, vol 6372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15928-2_37

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15928-2_37

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15927-5

  • Online ISBN: 978-3-642-15928-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation