Abstract Graph Transformation

Arend Rensink; D.S. Distefano

doi:10.1016/j.entcs.2006.01.022

Abstract Graph Transformation

Arend Rensink, D.S. Distefano

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

40 Citations (Scopus)

Abstract

Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.

Original language	English
Title of host publication	Proceedings of the Third International Workshop on Software Verification and Validation (SVV 2005)
Editors	S. Mukhopadhyay, A. Roychoudhury, Z. Yang
Publisher	Elsevier
Pages	39-59
Number of pages	21
ISBN (Print)	1571-0661
DOIs	https://doi.org/10.1016/j.entcs.2006.01.022
Publication status	Published - May 2006
Event	3rd International Workshop on Software Verification and Validation, SVV 2005 - Manchester, United Kingdom Duration: 31 Oct 2005 → 31 Oct 2005 Conference number: 3

Publication series

Name	Electronic Notes in Theoretical Computer Science
Publisher	Elsevier
Volume	157
ISSN (Print)	1571-0661
ISSN (Electronic)	1571-0661

Conference

Conference	3rd International Workshop on Software Verification and Validation, SVV 2005
Abbreviated title	SVV
Country	United Kingdom
City	Manchester
Period	31/10/05 → 31/10/05

Fingerprint

Keywords

Graph transformation
Software model checking
Abstract interpretation

Cite this

Rensink, A., & Distefano, D. S. (2006). Abstract Graph Transformation. In S. Mukhopadhyay, A. Roychoudhury, & Z. Yang (Eds.), Proceedings of the Third International Workshop on Software Verification and Validation (SVV 2005) (pp. 39-59). (Electronic Notes in Theoretical Computer Science; Vol. 157). Elsevier. https://doi.org/10.1016/j.entcs.2006.01.022

@inproceedings{0b1ff93e9e264d13842ee80d7c9d2430,

title = "Abstract Graph Transformation",

abstract = "Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.",

keywords = "Graph transformation, Software model checking, Abstract interpretation",

author = "Arend Rensink and D.S. Distefano",

year = "2006",

month = "5",

doi = "10.1016/j.entcs.2006.01.022",

language = "English",

isbn = "1571-0661",

series = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

pages = "39--59",

editor = "S. Mukhopadhyay and A. Roychoudhury and Z. Yang",

booktitle = "Proceedings of the Third International Workshop on Software Verification and Validation (SVV 2005)",

}

Rensink, A & Distefano, DS 2006, Abstract Graph Transformation. in S Mukhopadhyay, A Roychoudhury & Z Yang (eds), Proceedings of the Third International Workshop on Software Verification and Validation (SVV 2005). Electronic Notes in Theoretical Computer Science, vol. 157, Elsevier, pp. 39-59, 3rd International Workshop on Software Verification and Validation, SVV 2005, Manchester, United Kingdom, 31/10/05. https://doi.org/10.1016/j.entcs.2006.01.022

Abstract Graph Transformation. / Rensink, Arend; Distefano, D.S.

Proceedings of the Third International Workshop on Software Verification and Validation (SVV 2005). ed. / S. Mukhopadhyay; A. Roychoudhury; Z. Yang. Elsevier, 2006. p. 39-59 (Electronic Notes in Theoretical Computer Science; Vol. 157).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Abstract Graph Transformation

AU - Rensink, Arend

AU - Distefano, D.S.

PY - 2006/5

Y1 - 2006/5

N2 - Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.

AB - Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.

KW - Graph transformation

KW - Software model checking

KW - Abstract interpretation

U2 - 10.1016/j.entcs.2006.01.022

DO - 10.1016/j.entcs.2006.01.022

M3 - Conference contribution

SN - 1571-0661

T3 - Electronic Notes in Theoretical Computer Science

SP - 39

EP - 59

BT - Proceedings of the Third International Workshop on Software Verification and Validation (SVV 2005)

A2 - Mukhopadhyay, S.

A2 - Roychoudhury, A.

A2 - Yang, Z.

PB - Elsevier

ER -

Access to Document

10.1016/j.entcs.2006.01.022