Graph Construction and Matching for Imperative Programs using Neural and Structural Methods
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
TLDR
This paper introduces a pipeline that converts imperative programs and their annotations into typed, attributed graphs for scalable verification artefact reuse.
Key contributions
- Presents a pipeline to convert imperative programs and annotations into typed, attributed graphs.
- Integrates AST parsing with semantic embeddings from models like CodeBERT for rich graph representations.
- Demonstrates consistent graph construction across C, Java, and Dafny with various annotation styles.
- Provides a foundation for semantic enrichment and approximate graph matching for verification reuse.
Why it matters
Reusing verification artefacts is crucial for efficient software development. This paper provides a foundational method for representing programs and their specifications as graphs, enabling future work in scalable verification reuse. This could significantly reduce the effort in formal verification.
Original 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.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.