Personal tools

Falsifizierende Analysen

From PUMA Graduiertenkolleg

Jump to: navigation, search

Zusammenfassung

Die Korrektheit einer Behauptung, wie z.B. dass ein Programm eine Spezifikation implementiert, ist nur zu beweisen, wenn die Behauptung auch gilt. Um den Aufwand von Beweisversuchen falscher Behauptungen zu reduzieren, sind Techniken erforderlich, die zumindest in vielen Fällen falsche Annahmen als falsch belegen.

Das Auffinden von Laufzeitfehlern eines Systems bereits in einer frühen Phase verbessert und beschleunigt darüber hinaus die die Software-Entwicklung beträchtlich.

Das Ziel ist, neue Anwendungsbereiche für Model-checking, abstrakte Interpretation und Theorembeweisen oder ihre Kombinationen zu identifizieren, indem Falsifizierung für generellere Systembeschreibungen und ausdrucksstärkere Logiken betrachtet werden. Ziel ist dabei auch, Präzision und Überdeckung deutlich zu erhöhen.



Themen