用图结构统一表示多语言代码，助力验证资源复用
Graph Construction and Matching for Imperative Programs using Neural and Structural Methods
- 将代码与注释转为带类型属性的图，融合语法树与语义嵌入
- 跨语言（C/Java/Dafny）和注释风格生成一致图表示
- 适合做程序相似性分析与验证资产复用的研究者参考
重用验证成果需识别程序及其规格之间的结构与语义相似性。本文聚焦图构建这一基础步骤，提出一个将命令式程序及其注释转化为有类型、带属性图的流程。实验涵盖C语言的ACSL、Java的JML及Dafny程序数据集。该流程结合抽象语法树解析与SentenceTransformer、CodeBERT等模型生成的语义嵌入，生成同时体现结构关系与语义上下文的图表示。结果表明，可在不同语言和注释风格间构建一致的图表示。本工作为后续语义增强与近似图匹配在可扩展验证资源复用中的应用奠定了实用基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。