Graph Construction and Matching for Imperative Programs using Neural and Structural Methods

1. Probleemstelling

De kernuitdaging die wordt aangepakt, is het hergebruik van verificatieartefacten (specificaties, contracten en bewijzen) in software-engineering. Ondanks het bestaan van grote repositories van deze artefacten, blijft hun hergebruik grotendeels handmatig en inefficiënt. Ontwikkelaars worstelen met het vinden van relevante artefacten omdat bestaande oplossingen vaak verschillen in:

• Syntaxis: Verschillende programmeertalen (C, Java, C#) en specificatiestijlen (ACSL, JML, Dafny).
• Abstractie-niveaus: Variërende graden van detail in de implementatie.
• Domeinvocabulaire: Specifieke terminologie die semantische gelijkenis verduistert.

Huidige benaderingen vertrouwen vaak op handmatige aanpassing of eenvoudige syntactische matching, waardoor ze semantische correspondenties onder partiële equivalentie (waar slechts fragmenten van gedrag of intentie overeenkomen) niet kunnen vastleggen. De auteurs stellen voor om deze artefacten te representeren als getypeerde, geattributeerde grafen verrijkt met neurale semantische embeddings, waardoor deze kloof kan worden overbrugd en automatische ontdekking van structurele en semantische gelijkenissen mogelijk wordt.

2. Methodologie

Het paper presenteert een geünificeerde, end-to-end pijplijn die imperatieve programma's en hun annotaties omzet in grafrepresentaties, deze verrijkt met semantische data en gelijkenismatching uitvoert.

A. Datasetgeneratie en Transformatie

De onderzoekers startten met een basisdataset van 56 C-programma's (gecategoriseerd op structurele complexiteit: correct, voor de hand liggende verschillen, subtiele verschillen). Ze genereerden systematisch meertalige varianten met behulp van regelgebaseerde Python-scripts:

1. C + ACSL: C-programma's geannoteerd met de ANSI/ISO C Specificatietaal (ACSL).
2. Java + JML: C-programma's vertaald naar Java en geannoteerd met Java Modeling Language (JML).
3. C# + Dafny: C-programma's vertaald naar C# en vervolgens getransformeerd naar Dafny (een verificatiegerichte taal met ingebouwde specificaties).

B. Grafconstructie

De pijplijn converteert broncode en specificaties naar gerichte, getypeerde, geattributeerde grafen met behulp van networkx.

• Structuur: Knopen representeren syntactische elementen (variabelen, predicaten, besturingsflow, bewijsplichten) en randen representeren relaties (besturingsflow, dataflow, logische afhankelijkheden).
• Parsing:
  • C: Gebruikt clang.cindex (libclang) om Abstract Syntax Trees (AST's) te extraheren.
  • Java: Gebruikt javalang voor AST-extractie.
  • Dafny: Gebruikt regex-gebaseerde patroonmatching om methodesignaturen en specificaties te extraheren (vanwege het ontbreken van een standaardparser in de pijplijn).
• Specificatie-injectie: Cruciaal is dat formele specificaties (bijv. requires, ensures, invariant) niet zomaar tekst zijn; ze worden expliciet geïnjecteerd als dedicated knopen en gekoppeld aan hun corresponderende programmeerelementen binnen de graaf.

C. Semantische Verrijking (Neurale Embeddings)

Om betekenis verder dan syntaxis te vangen, integreert de pijplijn Large Language Models (LLM's):

• Tekstuele Linearisatie: Grafknopen worden geaggregeerd tot tekstuele sequenties.
• Embeddinggeneratie:
  • SentenceTransformer (all-MiniLM-L6-v2) wordt gebruikt voor de C-, Java- en C#-pijplijnen.
  • CodeBERT wordt gebruikt voor de Dafny-pijplijn.
• Vectoropslag: Deze modellen genereren dichte vector-embeddings die zowel syntactische patronen als latente semantische betekenis vangen (inclusief de intentie van de specificaties).

D. Grafmatching

Matching wordt uitgevoerd via paarsgewijze similariteitsberekening:

• Methode: Cosinus-similariteit wordt berekend tussen de embeddingvectoren van verschillende programmagrafen.
• Output: Een similariteitsscore (0.0 tot 1.0) wordt gegenereerd voor elk paar programma's, waardoor het rangschikken en ophalen van de meest semantisch en structureel vergelijkbare artefacten mogelijk wordt.

3. Belangrijkste Bijdragen

1. Geünificeerde Pijplijn: Een enkel, end-to-end framework voor het construeren en matchen van grafen over heterogene talen (C, Java, C#) en specificatiekaders (ACSL, JML, Dafny).
2. Geautomatiseerde Transformatie: Implementatie van regelgebaseerde scripts om specificatie-verrijkte datasets te genereren, waardoor structurele consistentie over talen heen wordt gewaarborgd.
3. Hybride Representatie: Een nieuwe techniek die zowel programmastructuur (via AST-gebaseerde grafen) als formele specificaties (via geïnjecteerde knopen) codeert in één enkele grafstructuur.
4. Neurale Integratie: Succesvolle integratie van transformer-gebaseerde modellen (SentenceTransformer, CodeBERT) om grafknopen te verrijken met semantische embeddings, waardoor similariteitsmatching mogelijk wordt die verder gaat dan token-niveau vergelijking.
5. Haalbaarheid over Talen: Aantonen dat consistente grafrepresentaties kunnen worden geconstrueerd om artefacten over verschillende taalecosystemen te matchen.

4. Resultaten

De experimenten werden uitgevoerd op de gegenereerde dataset (168 totale instanties over de categorieën).

• Similariteitsdistributie: Het systeem onderscheidde succesvol niet-verwante algoritmen (lage similariteitsscores, bijv. 0.35–0.60) van varianten van hetzelfde algoritme (hoge similariteitsscores, bijv. 0.80–0.95+).
• Semantische Sensitiviteit: Hoge scores werden waargenomen voor programma's met gedeelde algoritmische patronen (bijv. sorteren, zoeken), zelfs wanneer ze in verschillende talen waren geïmplementeerd of met verschillende specificatiestijlen.
• Impact van Specificaties: De opname van formele specificaties in de grafstructuur verbeterde de expressiviteit van de matching. Bijvoorbeeld, in de Dafny-dataset toonden "quicksort"-varianten zeer hoge similariteit (0.95–1.00), terwijl structureel verschillende algoritmen (bijv. insertion sort versus quicksort) een similariteit van bijna nul toonden.
• Robuustheid: Het systeem handteerde "spiegel"- en "unieke" varianten effectief, waarbij logische equivalentie werd geïdentificeerd ondanks oppervlakkige syntactische wijzigingen.

5. Betekenis en Toekomstig Werk

Betekenis:

• Schaalbaar Hergebruik: Dit werk biedt een praktische basis voor het automatiseren van het ophalen en aanpassen van verificatieartefacten, weg van handmatig zoeken.
• Semantische Matching: Door structurele grafen te combineren met neurale embeddings, adresseert de aanpak de "semantische kloof" die pure syntactische matching mist.
• Taalonafhankelijkheid: De pijplijn bewijst dat verificatieartefacten kunnen worden genormaliseerd naar een gemeenschappelijk graf-formaat, waardoor verificatie over talen heen wordt vergemakkelijkt.

Beperkingen & Toekomstige Richtingen:

• Afhankelijkheid van Parsing: De huidige aanpak vertrouwt sterk op regex en regelgebaseerde extractie (vooral voor Dafny), wat broos kan zijn voor complexe of niet-standaard code. Toekomstig werk heeft als doel volledige semantische parsing.
• Modelspecificiteit: De embedding-modellen zijn algemeen doelgericht en niet specifiek getraind op formele verificatieartefacten, wat mogelijk fijne semantische nuances mist.
• Volgende Stappen: De auteurs plannen om benaderende grafmatching-algoritmen en grafherherschrijf-technieken te integreren om niet alleen vergelijkbare artefacten te vinden, maar ze ook automatisch aan te passen en te verfijnen voor nieuwe contexten.

Kortom, dit paper zet een kritieke eerste stap richting Learning Infused Formal Reasoning (LIFR), en toont aan dat een hybride aanpak van structurele grafconstructie en neurale semantische verrijking een levensvatbaar pad is naar schaalbare, geautomatiseerde softwareverificatie.