Manipulation Boolescher Funktionen mit hybriden Datenstrukturen

Im Rahmen des Projektes soll sowohl die Kombination klassischer Methoden zu robusteren hybriden Beweisern als auch deren Erweiterung auf ein höheres Abstraktionsniveau untersucht und experimentell evaluiert werden.

Kontakt: Prof. Dr. Rolf Drechsler

Schaltungen werden zunehmend in sicherheitskritischen Bereichen eingesetzt. Dadurch kommt dem Korrektheitsnachweis eine immer wichtigere Rolle zu. Gleichzeitig nimmt die Komplexität der Schaltungen ständig zu. Nur formale Methoden können hier in Zukunft eine Garantie der Korrektheit liefern. Die klassischen Beweismethoden gelangen aber aufgrund der Problemkomplexität immer häufiger an ihre Grenzen, so dass eine Verbesserung der Verfahren notwendig ist. In Zusammenarbeit mit der Arbeitsgruppe aus Southampton sollen Methoden entwickelt werden, um die verschiedene Verifikationsansätze besser zu integrieren, aber auch um mit den Beweismethoden auf einem höheren Abstraktionsniveau -- der Wortebene anstatt der Booleschen Ebene -- anzusetzen.