Heuristic Search and Abstract Model Checking (R03)

• Subject Area: Software Engineering and Programming Languages
• Term: from 2004 to 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5485999

Ziel des Teilprojektes ist die Bekämpfung der Zustandsexplosion durch die Kombination zweier Ansätze:der Heuristischen Suche (also gerichtetes Model-Checking und Planungsverfahren aus derKünstlichen Intelligenz) und Abstraktion (in Kombination mit automatischer Abstraktionsverfeinerung).Das Leitmotiv des Vorhabens ist es, die beiden Ansätze zu kombinieren, indem die Suche aufAbstraktionen durch Heuristiken gelenkt wird, die durch das Lösen von Suchproblemen auf noch gröberenAbstraktionen berechnet wurden. Mit diesem Russische-Puppen-Prinzip ist das Projekt in derLage, informative Heurisiken effizient zu generieren, um sie rekursiv für die Suche zur Herleitungbesserer Abstraktionen und letztendlich zum Korrektheitsbeweis zu benutzen.

• DFG Programme: CRC/Transregios
• Subproject of: TRR 14: Automatic Verification and Analysis of Complex Systems
• Applicant Institution: Carl von Ossietzky Universität Oldenburg
• Co-Applicant Institution: Albert-Ludwigs-Universität Freiburg; Universität des Saarlandes
• Project Heads: Professor Dr. Bernd Finkbeiner; Professor Dr. Bernhard Nebel; Professor Dr. Andreas Podelski