Sebastian Wolff, Dr. rer. nat.
I have moved! You find more and up to date information on my:
I defended my PhD thesis titled Verifying Non-blocking Data Structures with Manual Memory Management in June 2021 with highest honors (summa cum laude). Before, I have been a PhD student at the Institute of Theoretical Computer Science (TCS) since September 2015 (TCS was formerly known as the Concurrency Theory Group at the University of Kaiserslautern, until late 2016). From 2015 to 2016 I was concurrently affiliated with the Competence Center High Performance Computing at Fraunhofer ITWM.
During my PhD I have developed the following model checkers:
- RocketScience: a tool that checks recursive integer programs for assertion errors.
- TMRexp: a static analysis tool for proving linearizability of concurrent, lock-free stacks and queues. This is the first tool to verify lock-free data structures with safe memory reclamation (hazard pointers and epoch-based reclamation).
- SEAL: model check for lock-free data structures with safe memory reclamation. This tool uses a type system to establish that memory is properly managed, allowing for the verification to be done under garbage collection semantics using an existing, off-the-shelf verifier.