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 Marko Doko (PhD student), Michalis Kokologiannakis (PhD student), Iason Marmanis (PhD student), Lovro Rozic (PhD student)

Alumni Soham Chakraborty (IIT Delhi), Ori Lahav (Tel Aviv University), Anton Podkopaev (JetBrains), Azalea Raad (Imperial College London)

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

Program committees 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

NETYS'21 BAM: Efficient model checking for barriers
NETYS'21 Verifying and optimizing the HMCS lock for Arm servers
ASPLOS'21 VSync: Push-button verification and optimization for synchronization primitives on weak memory models
ESOP'21 The decidability of verification under PS 2.0
POPL'21 PerSeVerE: Persistency semantics for verification under ext4 [Project page]
OOPSLA'20 Persistent Owicki-Gries reasoning [Project page]
ECOOP'20 Reconciling event structures with modern multiprocessors
PLDI'20 Promising 2.0: Global optimizations in relaxed memory concurrency [Project page]
ASPLOS'20 HMC: Model checking for hardware memory models
POPL'20 Persistency semantics of the Intel-x86 architecture [Project page]

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

Imprint | Data protection