Kurze Implementierungsbeispiele der abstrakten Interpretation

Question

Ich nehme einen Kurs über abstrakte Interpretation, aber ich habe keine Beispiele gesehen, wie die Theorie auf tatsächlichen Code abbildet.

Ich suche nach kurzen Codebeispielen, wo ich vorzugsweise nicht mit einem ganzen Compiler arbeiten muss. Die Analyse muss nicht nützlich sein, ich möchte nur ein Beispiel sehen, in dem die Analyse abgeleitet und dann implementiert wird.

Kennt jemand solche Beispiele, vielleicht von einem Universitätskurs?

Answer 1

Es gibt MonoREIL, die mit dem kürzlich geöffneten Tool BinNavi geliefert wird.

Siehe ist ein kurzes Intro.

Beachten Sie, dass der Kontext des MonoREIL-Frameworks keine Compiler, sondern die Analyse von Binärcode ist. Es wurde jedoch für reale Anwendungen verwendet, siehe Folie 34 ff. Der this Einführung (die mehr formalen Hintergrund enthält).

Answer 2

Es ist dieses Papier von Bertot

Structural abstract interpretation, A formal study using Coq

, die für eine einfache Spielzeug Sprache mit den Coq Proof-Assistenten eine vollständige Implementierung eines abstrakten Dolmetscher gibt. Ich benutzte dies für eine konkrete Referenz und fand es nützlich, wenn auch etwas schwierig, was angesichts der Thematik zu erwarten ist. Coq ist ein großartiges kleines Stück Software.

Ich kam in auch in einem Cousot Papier:

A gentle introduction to formal verification of computer systems by abstract interpretation

grobe Details (aber ich bin sicher, dass es nützlich Zitierungen für weitere Informationen sein) eine Implementierung in Astrée, ich bin nicht vertraut mit Astrée , also habe ich diesen Abschnitt nicht gelesen, aber ich denke, dass er deine Kriterien erfüllt.

Wenn Sie rüberkommen, lassen Sie es mich wissen! Besonders gerne würde ich einen abstrakten Prolog-Interpreter sehen.

Answer 3

AI basiert auf einer mathematischen Theorie Name Galois Verbindung. Die Theorie ist sehr einfach:

1. Zusammenfassung das Verhalten des Programms.
2. Führen Sie die Analyse auf der abstrakten Ebene durch.

Galois connection: Um das Actual und Abstract Programm betreffen.

This ist das beste Tutorial ich bisher über Abstrakte Interpretation gesehen habe:

Answer 4

Vielleicht dieses Tool auch für Sie interessant ist: Interproc Analyzer

Es ist ein abstrakter Analysator für eine sehr einfache Sprache, die jedoch bietet interprocedural Analysen. Sie können die Analyse ausprobieren und numerische Invarianten über das analysierte Programm erhalten. Der Quellcode ist verfügbar (OCaml).

Ein wirklich gründlicher und präziser Kurs, gegeben von einem der "Schöpfer" der abstrakten Interpretation, Patrick Cousot (bereits in einer der Antworten erwähnt): MIT course about Abstract Interpretation. Der Kurs bietet auch Aufgaben in OCaml.