Since October 2010, I am a researcher at MPI-SWS. Before that, I got my BA (2004) and PhD (2008) from the University of Cambridge, and was a postdoctoral researcher at Microsoft Research and at the University of Cambridge.

Research I am broadly interested in programming languages and verification with a focus on the following areas:

Group Ori Lahav (postdoc), Soham Chakraborty (PhD student), Marko Doko (PhD student)

Teaching Concurrency theory (SS2014), Concurrent program logics (SS2011)

Program committees 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, Cristiano Calcagno, Allen Clement, Hoang-Hai Dang, Dino Distefano, Mike Dodds, Derek Dreyer, Xinyu Feng, Alexey Gotsman, Tom Henzinger, Maurice Herlihy, Tony Hoare, Gil Hur, Suresh Jagannathan, Xiao Jia, Jan-Oliver Kaiser, Jeehoon Kang, Neel Krishnaswami, João Leitão, Cheng Li, Nuno Preguiça, Alan Mycroft, Chinmay Narayan, Aleks Nanevski, Georg Neis, Matthew Parkinson, Anton Podkopaev, Rodrigo Rodrigues, Peter Sewell, Ali Sezgin, Marc Shapiro, Francesco Zappa Nardelli, Beta Ziliani

Recent papers

ECOOP'17 Strong logic for weak memory: Reasoning about release-acquire consistency in Iris (with Kaiser, Dang, Dreyer, Lahav)
ECOOP'17 Promising compilation to ARMv8 (with Podkopaev, Lahav)
PLDI'17 Repairing sequential consistency in C/C++11 (with Lahav, Kang, Hur, Dreyer) [Project page]
ESOP'17 Tackling real-life relaxed concurrency with FSL++ (with Doko) [Project page]
CGO'17 Formalizing the concurrency semantics of an LLVM fragment (with Chakraborty) [Project page]
POPL'17 A promising semantics for relaxed-memory concurrency (with Kang, Hur, Lahav, Dreyer)
FM'16 Explaining relaxed memory models with program transformations (with Lahav) [Project page]
CGO'16 Validating optimizations of concurrent C/C++ programs (with Chakraborty) [Project page]
POPL'16 Taming release-acquire consistency (with Lahav, Giannarakis) [Project page]
POPL'16 Lightweight verification of separate compilation (with Kang, Kim, Hur, Dreyer) [Project page]
VMCAI'16 A program logic for C11 memory fences (with Doko) [Project page]

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