Two-level reasoning about graph transformation programs

Amani Makhlouf (1) , Christian Percebois (1) , Hanh Nhi Tran (1)

1 IRIT-ARGOS - Advancing Rigorous Software and System Engineering

This paper presents a method for verifying graph transformation programs written in Small-tALC, an imperative language which allows expressing graph properties and graph transformations in ALCQI description logic. We aim at reasoning not only about the local effect when applying a transformation rule on a matched subgraph but also about the global impact on the whole input graph when applying a set of rules. Using ALCQI assertional and terminological formulae to formalize directed labeled graphs, Small-tALC allows specifying local properties on individual nodes and edges as well as global properties on sets of nodes and edges. Our previous work focuses on verifying local properties of the graph. In this paper, we propose a static analyzer at terminological level that intertwines with a static analyzer at assertional level to infer global properties of the transformed graph.

Mots clés: Program verification; Abstract interpretation; Static analysis; Description logics; Graph transformation

Domaines: Logique en informatique [cs.LO]

Amani Makhlouf, Christian Percebois, Hanh Nhi Tran. Two-level reasoning about graph transformation programs. 12th International Conference on Graph Transformation (ICGT 2019), Jul 2019, Eindhoven, Netherlands. pp.111-127. ⟨hal-02451016⟩