Abstract:Reusing verification artefacts requires identifying structural and semantic similarities across programs and their specifications. In this paper, we focus on graph construction as a foundational step toward this goal. We present a pipeline that converts imperative programs and their annotations into typed, attributed graphs. Our experiments cover datasets including C with ACSL, Java with JML, and Dafny for C\#. The pipeline integrates abstract syntax tree parsing with semantic embeddings derived from models such as SentenceTransformer and CodeBERT. This enables the generation of graph representations that capture both structural relationships and semantic context. Our results show that consistent graph representations can be constructed across different languages and annotation styles. This work provides a practical basis for future steps in semantic enrichment and approximate graph matching for scalable verification artefact reuse.
| Comments: | 20 Pages. Technical Report. Maynooth University, Ireland. Submitted on 29 April 2026 |
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI) |
| ACM classes: | D.2.1; D.2.4; D.2.10; F.4.1; F.4.3 |
| Cite as: | arXiv:2604.26578 [cs.SE] |
| (or arXiv:2604.26578v1 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2604.26578 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Arshad Beg [view email]
[v1]
Wed, 29 Apr 2026 11:59:53 UTC (794 KB)