Graph Construction and Matching for Imperative Programs using Neural and Structural Methods
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Graph MatchingSimilar Papers 제목 키워드 기반
Terra: Imperative-Symbolic Co-Execution of Imperative Deep Learning Programs
Imperative programming allows users to implement their deep neural networks (DNNs) easily and has become an essential part of recent deep learning (DL) frameworks. Recently, several systems have been proposed to combine …
Deep LearningSpeculative Automated Refactoring of Imperative Deep Learning Programs to Graph Execution
Efficiency is essential to support ever-growing datasets, especially for Deep Learning (DL) systems. DL frameworks have traditionally embraced deferred execution-style DL code -- supporting symbolic, graph-based Deep Neu…
High-Order Relation Construction and Mining for Graph Matching
Graph matching pairs corresponding nodes across two or more graphs. The problem is difficult as it is hard to capture the structural similarity across graphs, especially on large graphs. We propose to incorporate high-or…
Graph MatchingRelationVocal Bursts Intensity PredictionJANUS: Fast and Flexible Deep Learning via Symbolic Graph Execution of Imperative Programs
The rapid evolution of deep neural networks is demanding deep learning (DL) frameworks not only to satisfy the requirement of quickly executing large computations, but also to support straightforward programming models f…
On oblivious branching programs with bounded repetition that cannot efficiently compute CNFs of bounded treewidth
In this paper we study complexity of an extension of ordered binary decision diagrams (OBDDs) called $c$-OBDDs on CNFs of bounded (primal graph) treewidth. In particular, we show that for each $k$ there is a class of CNF…