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.

Research on weak memory consistency Older research topics

Group Anton Podkopaev (part-time postdoc), Marko Doko (PhD student), Michalis Kokologiannakis (PhD student), Lovro Rozic (PhD student)

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

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

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

POPL'21 PerSeVerE: Persistency semantics for verification under ext4 (with Kokologiannakis, Kaysin, Raad)
OOPSLA'20 Persistent Owicki-Gries reasoning (with Raad, Lahav) [Project page]
ECOOP'20 Reconciling event structures with modern multiprocessors (with Moiseenko, Podkopaev, Lahav, Melkonian)
PLDI'20 Promising 2.0: Global optimizations in relaxed memory concurrency (with Lee, Cho, Podkopaev, Chakraborty, Hur, Lahav) [Project page]
ASPLOS'20 HMC: Model checking for hardware memory models (with Kokologiannakis)
POPL'20 Persistency semantics of the Intel-x86 architecture (with Raad, Wickerson, Neiger) [Project page]
OOPSLA'19 Weak persistency semantics from the ground up (with Raad, Wickerson) [Project page]
OOPSLA'19 Effective lock handling in stateless model checking (with Kokologiannakis, Raad) [Project page]
PLDI'19 Model checking for weakly consistent libraries (with Kokologiannakis, Raad) [Project page]
VMCAI'19 On the semantics of snapshot isolation (with Raad, Lahav) [Project page]
POPL'19 On library correctness under weak memory consistency (with Raad, Doko, Rožić, Lahav) [Project page]
POPL'19 Bridging the gap between programming languages and hardware weak memory models (with Podkopaev, Lahav) [Project page]
POPL'19 Grounding thin-air reads with event structures (with Chakraborty) [Project page]

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

Imprint | Data protection