Auf der Suche nach einem Buch, das eine Modellprüfanwendung ableitet und konstruiert

Question

Ich unterrichte mir die Programmüberprüfung und lerne derzeit Proof Assistenten. Ich habe das Buch Handbuch für praktische Logik und automatisierte Argumentation Dies gibt die Beweise für das Verständnis eines solchen Systems, aber vor allem für mich auch eine Implementierung der erforderlichen Algorithmen als OCAML -Quelle.

Ich weiß, dass einige der in aufgeführten Tools aufgeführt sind Wikipedia: Modellkontrollwerkzeuge und Yahoda: Überprüfungs -Tools -Datenbank sind Open Source, aber ich bevorzuge es auch, wenn die Theorie, Beweise, Algorithmen und Quellcode gleichzeitig vorgestellt werden, die sich gegenseitig verstärken, und in einem Fortschritt auf eine endgültige Anwendung aufzubauen.

Gibt es ein solches Buch für die Modellprüfung?

BEARBEITEN

Ich habe vielleicht gefunden, wonach ich suche Mathematische Logik für Informatik mit Prolog -Quelle. Weiß jemand, wenn ich das Buch nicht habe, ob dieses Buch zu der Anforderung passt?

Answer 1

John Harrisons Buch ist eine Ausnahme, um den ganzen Weg von Theorie zu Übung zu gehen und den gesamten Quellcode verfügbar zu machen. Ich denke, Sie werden es schwierig finden, ein äquivalentes Buch für die Modellprüfung zu finden, aber es gibt einige, die eine enge Annäherung erreichen.

• Prinzipien der Modellprüfung Von Baier und Katoen enthält viele Beispiele und eine ziemlich detaillierte algorithmische Beschreibung.
• Der Spin -Modellprüfer Von Gerard Holzmann ist eine ganz andere Behandlung des Autors eines der frühesten Modellprüfer. Er hat das Tool seit ungefähr dreißig Jahren beibehalten und hat einen "programmatischen" Ansatz.

Eine bessere Wette kann darin bestehen, die Kursnotizen und Laboraufgaben einiger online verfügbarer Kurse zu befolgen. Zumindest finden Sie die Theorie, Praxis und Beispiele, obwohl sie nicht in einem Buch organisiert sind.

• Edmund Clarkes Kurs in CMU hat eine Leseliste, die Tutorials für einige verschiedene Modellprüfer enthält.
• JOOST-PIETER KATOEN SOFTWARE-Verifizierungskurs und das Follow -up auf Praktische Modellprüfung und Erweiterte Modellprüfung Abdecken Sie viel Boden.

Schließlich ist dies nicht ganz das, wonach Sie gefragt haben, aber da Sie Logik und jetzt Modellüberprüfung studiert haben, werden Sie immer auf die abstrakte Interpretation beziehen, was die Grundlage für die statische Programmanalyse ist und eng mit der Modellüberprüfung verbunden ist (obwohl Diese Verbindung ist in der Modellprüfung nicht immer explizit).

• Patrick Cousots MIT -Kurs ist eine Tour de Force, die alles von gittertheoretische Fundamente bis hin zur vollständigen Implementierung eines statischen Analysators für eine einfache Sprache abdeckt. Sein Kursmaterial enthält alle Code und Übungen.