I am a tenured researcher at MPI-SWS, working in the area of programming languages and verification. I got my BA (2004) and PhD (2008) from the University of Cambridge, worked as a postdoctoral researcher at Microsoft Research and at the University of Cambridge, and joined MPI-SWS in October 2010.

Weak persistency (non-volatile memory, file systems) [ERC-CoG-2020 PERSIST] Weak consistency (weak memory models) Older research topics

Group Ellen Arlt (PhD student), Pavel Golovin (PhD student), Michalis Kokologiannakis (postdoc), Aristotelis Koutsouridis (PhD student), Iason Marmanis (PhD student), Léo Stefanesco (Postdoc)

Alumni Soham Chakraborty (TU Delft), Marko Doko (Heriot-Watt University), Ori Lahav (Tel Aviv University), Anton Podkopaev (JetBrains), Azalea Raad (Imperial College London)

Teaching Weak memory consistency (2022), Marktoberdorf 2019, Weak memory consistency (2017), Concurrency theory (SS2014), Concurrent program logics (SS2011)

Program committees ESOP 2025 (chair), OOPSLA 2023, CPP 2023, OOPSLA 2021, PLDI 2021, PPoPP 2021 (ERC), POPL 2021, ESOP 2020, OOPSLA 2019 (ERC), PPoPP 2019, POPL 2018, CPP 2018, ESOP 2017, CPP 2017 (co-chair), POPL 2017 (ERC), ITP 2016, CAV 2016 (ERC), NETYS 2016, TASE 2016, PDP/4PAD 2016, ICFEM 2015, TASE 2015, PDP/4PAD 2015, Coq 2014 (co-chair), ICFEM 2014, POPL 2014, Coq 2013, ICFEM 2013, SEFM 2013, PCI 2013, TASE 2013, PLDI 2013 (ERC), POPL 2013 (ERC), ICFEM 2012, SEFM 2012, CPP 2011, APLAS 2011, ICFEM 2011, CAV 2011, VS-Theory 2010, FTfJP 2010

Some collaborators Thibaut Balabonski, Josh Berdine, Byron Cook, Allen Clement, Hoang-Hai Dang, Dino Distefano, Mike Dodds, Derek Dreyer, Xinyu Feng, Philippa Gardner, Alexey Gotsman, Tom Henzinger, Maurice Herlihy, Gil Hur, Suresh Jagannathan, Xiao Jia, Jan-Oliver Kaiser, Jeehoon Kang, Neel Krishnaswami, Ori Lahav, João Leitão, Cheng Li, Nuno Preguiça, Alan Mycroft, Chinmay Narayan, Aleks Nanevski, Georg Neis, Matthew Parkinson, Anton Podkopaev, Rodrigo Rodrigues, Konstantinos Sagonas, Peter Sewell, Ali Sezgin, Marc Shapiro, Francesco Zappa Nardelli, Beta Ziliani

Recent papers

PLDI'24 SPORE: Combining symmetry and partial order reduction
TACAS'24 Enhancing GenMC's usability and performance
ESOP'24 Specifying and verifying persistent libraries
FMCAD'23 Optimal bounded partial order reduction
CAV'23 Unblocking dynamic partial order reduction
OSDI'23 BWoS: Formally verified block-based work stealing for parallel processing
TACAS'23 Reconciling preemption bounding with DPOR
ASPLOS'23 AtoMig: Automatically migrating millions lines of code from TSO to WMM
POPL'23 Kater: Automating weak memory model metatheory and consistency checking
POPL'23 The path to durable linearizability
VSTTE'22 SMT-based verification of persistency invariants of Px86 programs
OOPSLA'22 Model checking for a multi-execution memory model
POPL'22 Truly stateless, optimal dynamic partial order reduction
POPL'22 Extending Intel-x86 consistency and persistency

[All publications...] [By subject...] [@DBLP] [@GoogleScholar]

Imprint | Data protection