Inkrementelles SAT und SMT für skalierbare Verifikation

Computer, Telefone, Smart Devices und die darauf laufenden Anwendungen (Apps) sind allgegenwärtig und begleiten uns rund um die Uhr. Diese Technologien sind zu einem wesentlichen Bestandteil unseres täglichen Lebens geworden, daher ist es sehr wichtig, sicherzustellen, dass sie immer wie vorgesehen funktionieren. Formale Verifikation bietet Techniken, um zu zeigen, dass sich ein Hardware- oder Softwaresystem unter allen möglichen Umständen genau so verhält, wie es ursprünglich geplant war. Viele dieser Verifikationstechniken, zum Beispiel Model Checking oder symbolische Ausführung, müssen wiederholt logische Probleme lösen, die sich sehr ähnlich sind, um die Korrektheit eines Systems zu zeigen oder zu widerlegen. Der Fokus dieses Projekts liegt auf diesen zugrunde liegenden logischen Problemen. Inkrementelle Lösungsverfahren versuchen, die Ähnlichkeit der auftretenden logischen Probleme auszunutzen, um mit weniger Aufwand Lösungen zu finden. Das Ziel dieses Projekts ist es, verbesserte inkrementelle Lösungsmethoden für unsere logischen Probleme einzuführen und damit die Grenzen formaler Verifikationstechniken zu verschieben.

Wir nutzen moderne Technologie für fast alles - Kommunikation, Transport, Arbeit, Einkaufen, Unterhaltung und mehr. Aber wie können wir sicher sein, dass die Systeme, auf die wir uns verlassen, immer richtig funktionieren? Da wir immer mehr Software und Hardware verwenden, wird es immer wichtiger, sicherzustellen, dass sie korrekt sind. Eine Möglichkeit dies zu erreichen, besteht darin ihr Verhalten mit logischen Formeln zu beschreiben und dann spezialisierte automatisierte Beweissysteme zu verwenden, um zu überprüfen, ob sie in allen möglichen Situationen korrekt funktionieren. Ziel dieses Projekts war es, diese Beweissysteme effizienter, vielseitiger und zuverlässiger zu machen. In den letzten drei Jahren haben wir mehrere wichtige Fortschritte erzielt. Wir haben standardisierte Methoden entwickelt, damit diese Beweissysteme besser zusammenarbeiten, was ihre Nutzung in größeren Systemen erleichtert und ihre zukünftige Entwicklung und Wartung vereinfacht. Wir haben auch neue Techniken entwickelt, um komplexe logische Probleme - wie die Beschreibung von Hardware-Schaltungen - zu vereinfachen, sodass sie effizienter gelöst werden können. Darüber hinaus haben wir einen neuen Ansatz entwickelt, um verteilte Protokolle zu überprüfen - Regelwerke, die es den Komponenten verteilter Systeme ermöglichen, miteinander zu kommunizieren - indem wir ihre eingebauten Symmetrien nutzen. Um das Vertrauen in automatisierte Beweissysteme weiter zu stärken, haben wir neue Methoden implementiert, die sicherstellen, dass die Lösungen, die sie produzieren, korrekt und zuverlässig sind. Diese Verbesserungen fördern die Weiterentwicklung der formalen Verifikation und machen es einfacher und effizienter, nachzuweisen, dass kritische Systeme, wie medizinische Geräte oder selbstfahrende Autos, korrekt und sicher funktionieren. Durch die Verbesserung dieser Verifikationswerkzeuge trägt unsere Forschung dazu bei, alltägliche Technologie zuverlässiger zu machen und das Risiko von Softwarefehlern und Systemausfällen zu verringern.