AI Insight
This paper presents a computational pipeline that converts imperative programs and their formal specifications into typed, attributed graphs by combining abstract syntax tree parsing with semantic embeddings from neural language models like SentenceTransformer and CodeBERT. The researchers tested their approach on multiple programming languages including C with ACSL annotations, Java with JML, and Dafny, demonstrating that consistent graph representations can be generated across different languages and annotation styles. This graph construction method serves as a foundation for future work in verification artefact reuse, enabling structural and semantic comparison of programs.
Why it matters
This work addresses a critical challenge in software verification by providing a systematic way to identify and reuse verification artefacts across different codebases. The ability to automatically match similar program structures and semantics could significantly reduce the time and effort required for formal verification, making it more practical for large-scale software development projects.
Understand the Science
arXiv:2604.26578v3 Announce Type: replace-cross
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 programs. 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.
Source: Graph Construction and Matching for Imperative Programs using Neural and Structural Methods