I was the lead developer of Gobra, a verifier for Go programs, which serves as a platform to apply my research results to real-world software. Gobra has been a core component of numerous collaborations, including ETH's VerifiedScion project and the Centre for Cyber Trust

We used Gobra to verify that the implementation of the Scion border router is memory-safe, crash free, data-race free, and adheres to the formal Scion protocol. My techniques for scaling verification were key enablers in verifying 4,700 lines of production code using Gobra.

We verified an implementation of the WireGuard protocol. My contributions enabled us to combine automated protocol verification with automated program verification targeting real-world code. In addition to protocol adherence, I verified that no confidential protocol data is leaked.

Automated Verification of Advanced Correctness and Security Properties

Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router

J. C. Pereira, T. Klenze, S. Giampietro, M. Limbeck, D. Spiliopoulos, F. A. Wolf, M. Eilers, C. Sprenger, D. Basin, P. Müller, A. Perrig

Verifiable Security Policies for Distributed Systems

F. A. Wolf, P. Müller

Sound Verification of Security Protocols: From Design to Interoperable Implementations

L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. Wiesner, D. Basin, P. Müller

Code-Level Verification (The Complete Guide to SCION)

L. Arquint, P. Müller, W. Oortwijn, J. C. Pereira, F. A. Wolf

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA

F. A. Wolf, M. Schwerhoff, P. Müller

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA

F. A. Wolf, M. Schwerhoff, P. Müller

Gobra: Modular Specification and Verification of Go Programs

F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. C. Pereira P. Müller

Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification

F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. C. Pereira P. Müller

Traveling

The completion of my doctorate offered a unique opportunity for more involved travel. The three core components of my travel were: (1) a hike from France to the west coast of Spain spanning ca. 900 km, (2) a journey by train to Istanbul through eastern Europe, and (3) extensive travel through Mainland China, Hong Kong, Macau, Taiwan, and Japan.

Research Assistant

My research focused on applying formal verification to real-world security-critical software. Within this focus, I developed techniques to verify that information-flow policies are satisfied, policies specify the intended behavior, security protocols are implemented correctly, and concurrent code functions correctly.

Head Teaching Assistant

Head Teaching Assistant of the course ‘Introduction to Programming’ for computer science students. The course teaches the basic concepts of Object-Oriented Programming using Java.

My responsibilities consisted of:

• managing a team of 30+ teaching assistants
• supporting 600+ students with technical and administrative matters
• designing and developing assignments and instructional material
• organizing, conducting, and grading exams

Teaching Assistant

My responsibilities consisted of preparing and conducting exercise sessions.

Doctorate in Computer Science

Advisor: Peter Müller, Programming Methodology Group

Doctoral Thesis: Automated Verification of Advanced Correctness and Security Properties [pdf]

MSc in Computer Science

Core Subjects: Security Engineering, Network Security, Formal Methods for Information Security, Advanced Compiler Design, Design of Parallel and High-Performance Computing

Master Thesis: Verifying Fine-Grained Concurrent Data Structures

GPA: 5.64/6

BSc in Computer Science

GPA: 5.48/6