Wortbasiertes Reasoning mit Computeralgebra und SAT

Formale Verifikation zielt darauf ab, die Korrektheit von komplexen Systemen, Hardware-Designs und Software zu gewährleisten. Im Gegensatz zu traditionellen Testmethoden, die sich auf die Ausführung von Testfällen und die Beobachtung von Ausgaben stützen, werden bei der formalen Verifikation präzise mathematische und logische Schlussfolgerungen eingesetzt, um die Systemeigenschaften zu validieren und so zu gewährleisten, dass sie die festgelegten Anforderungen und Standards erfüllen. In der Tat ist formale Verifikation in der modernen Ingenieurspraxis unerlässlich, da sie die Konstruktion robuster und zuverlässiger Systeme ermöglicht, die hohe Qualitäts-, Sicherheits- und Schutzkriterien erfüllen. Die erfolgreiche Entwicklung ausgefeilter automatischer Argumentationswerkzeuge für das Erfüllbarkeitsproblem der Aussagenlogik (SAT) und Computeralgebra-Algorithmen eröffneten neue Perspektiven und Herausforderungen für die formale Verifikation. Obwohl sowohl SAT-Solving als auch Computeralgebra auf eine lange Geschichte zurückblicken, wurden sie bisher meist getrennt voneinander zur Problemlösung eingesetzt. Aufgrund der fehlenden engen Integration ist es derzeit nicht möglich, die Stärken beider Ansätze gleichzeitig in einer einzigen Methode zu nutzen. Das Ziel dieses Projekts ist es, neue bitgenaue formale Verifikationstechniken zu entwickeln. Wir kombinieren SAT und Computeralgebra, um einzigartige SAT-basierte algebraische Methoden für Schlussfolgerungen auf Wortebene über Polynome zu entwerfen. In diesem Fall beschreiben Wörter Vektoren und Bitfolgen, die z.B. Teile des Computerspeichers abbilden. Während wir das breite Gebiet der Computeralgebra diskutieren, müssen wir jedoch unseren Fokus auf ausgewählte Polynomringe legen. Wir konzentrieren uns auf die Integration von SAT-Solving in algebraische Schlussfolgerungen über pseudo-boolesche Polynome, die zum Beispiel zur Verifikation von Hardware-Schaltungen verwendet werden, sowie Polynome über endliche Domänen, die zur Modellierung von Computerspeichern und kryptographischen Kodierungen verwendet werden können. Um die entwickelten Methoden validieren zu können, entwickeln wir zusätzlich Techniken zur Zertifizierung der Verifikationsergebnisse. Wir sind somit in der Lage, eine zusätzliche Vertrauensebene bereitzustellen. Die Weiterentwicklung formaler Methoden ist unverzichtbar, und wir glauben, dass die Verknüpfung dieser orthogonalen Argumentationsansätze ein wichtiger Schritt in diese Richtung ist. Durch die enge Verknüpfung von Computeralgebra und SAT-Solving können wir das Potenzial beider Techniken voll ausschöpfen und die Kapazität moderner Methoden zur Argumentation über endliche Körper, Bitvektoren oder pseudo-boolesche Polynome erheblich steigern. Der Erfolg dieses Projekts wird einzigartige theoretische und praktische Lösungen mit praktischen Anwendungen in den Bereichen Hardwareverifikation, Blockchain-Technologie und Post-Quantum- Kryptographie hervorbringen.