Abstraktionstechniken zur Verifikation lokaler Eigenschaften großer paralleler Systeme

• Applicant: Professorin Dr. Heike Wehrheim
• Subject Area: Software Engineering and Programming Languages
• Term: from 2008 to 2013
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 79848547

• Final Report Year: 2012

Final Report Abstract

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.

Publications

• 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