Veröffentlichung im Rahmen des 26. Workshops "Programmiersprachen und Rechenkonzepte" der Gesellschaft für Informatik Anfang Mai 2009.

Abstract: Symbolische Modelle definieren Zustandssysteme, welche zur Software-Modell-Prüfung, zum Modell basierten Testen und zur Codegenerierung genutzt werden können. Die Größe und Komplexität dieser Modelle sind dabei entscheidende Einflussfaktoren und sollten möglichst vereinfacht werden. Aus Quellcode gewonnene Modelle in Form von symbolischen Kellersystemen (SPDS) erlauben nicht nur präzisere Ergebnisse, sondern führen auch ohne Modellexplosion bei exakter Nachbildung von Rekursion zu weniger Fehlalarmen. Für diese SPDS wurden zwei verschiedene Ansätze verfolgt, die die innere Struktur der Zustände ausnutzen, um den Zustandsraum der Modelle weiter zu verkleinern. Eigene Experimente zeigen, dass diese die Modellprüfung erheblich beschleunigen bzw. die Modellprüfung erst ermöglichen.

Download: rp09.pdf