Zertifizierte Computersysteme werden zunehmend zum Schlüssel für die immer komplexeren Entscheidungsprozesse in unserer modernen Gesellschaft. Fehlerfreie und sichere Lösungen sind unter anderem in Bereichen wie Künstlicher Intelligenz (KI), autonomen Systemen, Big Data, Blockchain, Dezentraler Finanzen (DeFi) oder Cloud Computing unverzichtbar. Während die explosionsartige Zunahme an Anwendungen von Computersystemen zu enormen Steigerungen von Produktivität, Wohlstand und Komfort führt, entsteht eine paradoxe Situation: Wir verlassen uns auf Computersysteme, obwohl unzählige Szenarien zeigen, dass diese Systeme nicht (ausreichend) zertifiziert sind und daher fehleranfällig sein können. Das Gebiet des Automated Reasoning bietet computergestützte Lösungen, um zu beweisen, dass Computersysteme fehlerfrei sind – ähnlich wie man mathematische Theoreme beweist. Doch wer sagt Softwareentwickler:innen, welche automatisierten Beweismethoden eingesetzt werden sollten? Und welche Methode eignet sich am besten für Code Reviews, um die Sicherheit und Zuverlässigkeit eines Systems zu gewährleisten? Dieser Vortrag beleuchtet einige Herausforderungen des automatisierten Schließens und konzentriert sich auf konkrete Anwendungsbeispiele der Systemverifikation. Dabei werden Aspekte der Open-Source-Softwareentwicklung hervorgehoben, die es ermöglichen, unsere Lösungen unkompliziert in andere Technologien zu integrieren – ohne dass Nutzer:innen selbst Expert:innen im Bereich des Automated Resaoning sein müssen.

Certified computer systems are becoming the key in the increasingly complex decision making activities of our modern society. Among others, error-free and secure solutions are indispensable within AI, Autonomous Systems, Big Data, Blockchain, Decentralized Finance (DeFi), or Cloud Computing. While the explosion in applications of computer systems leads to great increases in productivity, wealth, and convenience, it creates a paradoxical situation: we rely on computer systems despite that uncountable many scenarios showcase that computer systems are not (properly) certified and hence are error-prone. The area of automated reasoning provides computer-aided solutions to prove that computer systems are error-free, just like we prove theorems in mathematics. However, who can tell software developers which automated reasoning solutions should be used? Moreover, which reasoning method is best to be used during code review, for ensuring system safety and security? This talk will reflect on some challenges of automated reasoning and focus on concrete applications of system verification security. We will highlight aspects of open-source code development, allowing others to easily use our solutions in their technologies without the need of becoming experts in automated reasoning.