smackers/smackModulare Software-Verifikations-Toolchain, die LLVM IR in die Boogie-Zwischenverifikationssprache übersetzt, um begrenzte und experimentelle unbegrenzte Assertionsprüfungen in C-Programmen durchzuführen.
SMACK ist sowohl eine modulare Software-Verifizierungswerkzeugkette als auch ein eigenständiger Software-Verifizierer. Es kann verwendet werden, um die Annahmen (assertions) in seinen Eingabeprogrammen zu verifizieren. Im Standardmodus werden Annahmen bis zu einer bestimmten Grenze von Schleifeniterationen und Rekursionstiefe verifiziert; es enthält experimentelle Unterstützung für unbeschränkte Verifizierung. SMACK handhabt komplexe Merkmale der Sprache C, einschließlich dynamischer Speicherzuweisung, Zeigerarithmetik und bitweiser Operationen.
Unter der Haube ist SMACK ein Übersetzer von der beliebten LLVM-Compiler-Zwischendarstellung (IR) in die Boogie Zwischenverifikationssprache (IVL). Die Verwendung von LLVM IR nutzt eine wachsende Anzahl von Compiler-Frontends, Optimierungen und Analysen. Derzeit unterstützt SMACK nur die Sprache C über den Clang-Compiler, obwohl wir daran arbeiten, Unterstützung für weitere Sprachen bereitzustellen. Die Ausrichtung auf Boogie nutzt eine kanonische Plattform, die die Implementierung von Algorithmen zur Verifikation, Modellprüfung und abstrakten Interpretation vereinfacht. Derzeit nutzt SMACK die Verifikationswerkzeuge Boogie und Corral.
Siehe unten für Systemanforderungen, Installation, Verwendung und alles Weitere.
Wir sind sehr an Ihren Erfahrungen mit der Nutzung von SMACK interessiert. Bitte kontaktieren Sie Zvonimir, Michael oder Shaobo mit eventuellem Feedback.
Bei allgemeinen Fragen konsultieren Sie zunächst die FAQ.
Wenn etwas defekt ist oder fehlt, öffnen Sie ein Issue.
Als letzte Möglichkeit senden Sie eine E-Mail an Michael, Zvonimir und Shaobo.
Um über Aktualisierungen informiert zu bleiben, können Sie SMACKs Github-Seite beobachten (watch).
Das SMACK-Projekt wurde teilweise durch Fördermittel der National Science Foundation, VMware, Amazon und Microsoft Research unterstützt. Wir verlassen uns auch auf die Infrastruktur des Emulab der University of Utah für umfangreiche Benchmarking von SMACK.
