Contact:
60 Fifth Avenue
Room 442
New York, NY 10011
(map)

About Me

I am on the job market, looking for opportunities to apply formal methods and verification to real-world industrial problems.
Résumé    CV

I'm a Junior Fellow of the Simons Foundation and post-doctoral researcher in the Analysis of Computer Systems Group at New York University's Courant Institute, working with Thomas Wies. Before, I obtained my PhD from the University of Braunschweig, Germany, under the supervision of Roland Meyer.

My research revolves around the analysis and verification of concurrent programs. I am specifically interested in the automated verification of high-performance data structures. During my PhD, I have contemplated about the manual memory management aspect of non-blocking data structures and how to verify it separately. Currently, I am focusing on progressing the state of the art in automatic verifiers for garbage collected data structures.

Publications

  1. nekton: A Linearizability Proof Checker
    Artifacts Available and Functional
    Roland Meyer, Anton Opaterny, Thomas Wies, and Sebastian Wolff
    CAV 2023
    PDF DOI
  2. Embedding Hindsight Reasoning in Separation Logic
    Artifacts Available and Evaluated&Reusalbe
    Roland Meyer, Thomas Wies, and Sebastian Wolff
    PLDI 2023
    PDF Slides arXiv DOI Project Page
  3. Make flows small again: revisiting the flow framework
    Artifacts Available and Evaluated&Reusalbe
    Roland Meyer, Thomas Wies, and Sebastian Wolff
    TACAS 2023
    PDF Slides arXiv DOI Artifact Project Page
  4. Model-Based Fault Classification for Automotive Software
    Mike Becker, Roland Meyer, Tobias Runge, Ina Schaefer, Sören van der Wall, and Sebastian Wolff
    APLAS 2022
    PDF arXiv DOI
  5. A concurrent program logic with a future and history
    Artifacts Available and Evaluated&Reusalbe
    Roland Meyer, Thomas Wies, and Sebastian Wolff
    OOPSLA 2022
    PDF Slides arXiv DOI Artifact Project Page
  6. Verifying Non-blocking Data Structures with Manual Memory Management
    ETAPS 2022 Doctoral Dissertation Award
    Sebastian Wolff
    PhD thesis, 2021
    PDF Slides Animated Slides Deposited Version Additional Material
  7. Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
    Artifacts Available and Evaluated&Reusalbe
    Roland Meyer and Sebastian Wolff
    POPL 2020
    PDF Slides arXiv DOI Project Page
  8. Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
    Artifacts Available and Evaluated&Reusalbe
    Roland Meyer and Sebastian Wolff
    POPL 2019
    PDF Slides arXiv DOI Project Page
  9. Reasoning About Weak Semantics via Strong Semantics
    Roland Meyer and Sebastian Wolff
    Principled Software Development—Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday, 2018
    PDF DOI
  10. Effect Summaries for Thread-Modular Analysis
    Lukáš Holík, Roland Meyer, Tomáš Vojnar, and Sebastian Wolff
    SAS 2017
    PDF Slides arXiv DOI Code
  11. Pointer Race Freedom
    Frédéric Haziza, Lukáš Holík, Roland Meyer, and Sebastian Wolff
    VMCAI 2016
    PDF arXiv DOI

Community Service

Artifact Evaluation Chair
VMCAI 2024; ESOP 2023
Reviewer
POPL 2024; TACAS 2024; VMCAI 2024; PLDI 2022; CONCUR 2021; ESOP 2020; FSTTCS 2020; Petri Nets 2020; APLAS 2019; ESOP 2019; FORTE 2019; NETYS 2019; TACAS 2019; CONCUR 2018; FoSSaCS 2018; ATVA 2017; CONCUR 2017; MFCS 2017; NETYS 2016; TACAS 2016
Acta Informatica; Computing; Concurrency and Computation: Practice and Experience (CCPE); Science of Computer Programming (SCP)
Artifact Evaluation Committee
VMCAI 2022; POPL 2021; ATVA 2019
Misc
ETAPS 2023 Doctoral Dissertation Award Committee