Veröffentlichung bei der Konferenz Software Engineering 2012 für die Arbeitstagung Programmiersprachen (ATPS'12) in Berlin.

Abstract: Viele Aussagen zum Programmverhalten sind in turingmächtigen Programmiersprachen unentscheidbar (Rice Theorem). Mittels Abstraktion vom Programmverhalten können nicht-turingmächtige Modelle automatisch erzeugt werden. Modelle in Form von symbolischen Kellersystemen (SPDS) erlauben eine so präzise Darstellung des Programmverhaltens, so dass eine ISO-C konforme Semantik möglich ist. Allerdings führen präzisere Darstellungen auch zu komplexeren und umfangreicheren Modellen. Dies erschwert Software-Modellprüfung, modellbasiertes Testen und Testdaten- und Codegenerierung. Mehr Abstraktion führt hingegen zu kleineren Modellen, allerdings auch zu mehr Fehlalarmen. Ziel dieser Arbeit ist es, bezüglich temporaler Aussagen unwichtige Teile eines SPDS zu identifizieren und von diesen Teilen so zu abstrahieren, dass keine Fehlalarme entstehen.

Download: atps12.pdf