Formal Verification: Increased Security for Software and Hardware through Logic and Mathematics
Dr. Sebastian Ertel, researcher and head of the Verified System Design Automation research group, at the Barkhausen Institut, was a guest on the Cyberagentur podcast “Per Anhalter durch den Cyberraum” (“Hitchhiking Through Cyberspace”). In conversation with podcaster Marcel Roth and Dr. Dirk Pollmächer from the Cyberagentur, the discussion focuses on a topic that is often overlooked in public discourse but is essential for the security of digital systems: formal verification.
Formal verification uses mathematical methods to systematically analyze and verify software and hardware systems. Its goal is to prove that programs behave exactly as intended and do not enter unintended or unsafe states. This approach is becoming increasingly important, especially for complex and safety-critical applications.
In the podcast, Sebastian Ertel explains why formal methods are key to building trust in digital technologies and how they can also be applied in the context of artificial intelligence. At the same time, the conversation highlights that behind computer science and mathematics lie fundamental questions that go beyond purely technical considerations.
Listen to the full episode “Making Hardware and Software Secure - with Logic and Math.” (only german)