Abstrakt. Vi visar hur man formaliserar en begränsningsbaserad data ow analys i den specifika språk Coq bevis assistent. Det handlar om att definiera en beroende typ av gitter tillsammans med ett bibliotek av lattice functors för modulärt byggande av komplexa abstrakta domäner. Restriktioner uttrycks i en mellanrepresentation som möjliggör både eektiv begränsningsupplösning och korrekta bevis på analysen med avseende på en operationell semantik. Beviset på att det finns en korrekt, minimal lösning på begränsningarna är konstruktivt, vilket innebär att extraktionsmekanismen hos Coq ger en bevisligen korrekt data ow analysator i ocaml. Biblioteket av gitter tillsammans med den mellanliggande representationen av begränsningar de neras på ett analys-oberoende sätt som ger en grund för ett generiskt ramverk för att bevisa och extrahera statiska analysatorer i Coq.
REF är en utdragbar dataflödesanalys i Coq i samband med Java.
Extracting a Data Flow Analyser in Constructive Logic
{'venue': 'ESOP', 'journal': None, 'mag_field_of_study': ['Computer Science']}