Abstraktionstechniken zur Verifikation lokaler Eigenschaften großer paralleler Systeme

• Antragstellerin: Professorin Dr. Heike Wehrheim
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2008 bis 2013
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 79848547

• Erstellungsjahr: 2012

Zusammenfassung der Projektergebnisse

In diesem Projekt ist ein Abstraktionsverfahren für parallele Programme konzipiert, als korrekt bewiesen und implementiert worden. Dieses Verfahren verbindet eine dreiwertige Prädikatabstraktion mit einer Spotlightabstraktion. Für die Abstraktionsverfeinerung ist eine neuartige heuristische Technik entwickelt worden. Sie berücksichtigt den Grad der Abhängigkeit zwischen Prozessen in einer Parallelkomposition und basiert auf der Generierung mehrerer Gegenbeispiele. Insgesamt sind damit alle Teilziele aus dem Projektantrag erreicht worden.

Projektbezogene Publikationen (Auswahl)

• Bounded Model Checking for Partial Kripke Structures. In: Fitzgerald, John S.; Haxthausen, Anne E.; Yenigun, Husnu (eds.): Theoretical Aspects of Computing - ICTAC 2008, 5th International Colloquium. Springer, LNCS, vol. 5160 , pp. 380-394 (2008)
  Heike Wehrheim
  
• Three-Valued Spotlight Abstractions. In: Ana Cavalcanti and Dennis Dams (eds.): FM 2009: Formal Methods. Springer, LNCS, vol. 5850, pp. 106-122 (2009)
  Jonas Schrieb, Heike Wehrheim, Daniel Wonisch
  
• On Symmetries and Spotlights - Verifying Parameterised Systems. In: J.S. Dong, H.Zhu (eds.): ICFEM 2010. Springer Verlag Berlin-Heidelberg, LNCS, vol. 6447, pp. 534- 548 (2010)
  Nils Timm, Heike Wehrheim
  
• Weaving-Based Configuration and Modular Transformation of Multi-Layer Systems. In: Robert France, Jürgen Kazmeier, Colin Atkinson, Ruth Breu (eds.): Models 2012. Springer Verlag, LNCS 7590, pp. 776-792 (2012)
  Galina Besova, Sven Walther, Heike Wehrheim, Steffen Becker