PL/Verification @ MPI-SWS


Concurrent program logics

Since October 2010, I am a tenure-track researcher at MPI-SWS working on software verification. Previously, I was a post-doctoral researcher at the University of Cambridge Computer Laboratory and Microsoft Research Cambridge. My undergraduate studies and PhD were both at the University of Cambridge.

I am generally interested in programming languages and verification with an emphasis on concurrency. The main focus areas of my work so far have been:

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

Current students Soham Chakraborty, Marko Doko, Mustafa Zengin.

Some coauthors Josh Berdine, Byron Cook, Cristiano Calcagno, Dino Distefano, Mike Dodds, Derek Dreyer, Xinyu Feng, Alexey Gotsman, Tom Henzinger, Maurice Herlihy, Tony Hoare, Gil Hur, Suresh Jagannathan, Neel Krishnaswami, Alan Mycroft, Chinmay Narayan, Aleks Nanevski, Georg Neis, Matthew Parkinson, Peter Sewell, Ali Sezgin, Marc Shapiro, Francesco Zappa Nardelli, Beta Ziliani.

Recent papers

Subm. GPS: Navigating weak-memory with ghosts, protocols, and separation. (with Turon, Dreyer) [Project page] [Earlier TR]
Tech.rep. A logical step forward in parametric bisimulations (with Hur, Neis, Dreyer) [Project page]
OOPSLA'13 Relaxed separation logic: a program logic for C11 concurrency (with Narayan) [Project page]
ICFP'13 Mtac: a monad for typed tactic programming in Coq (with Ziliani, Dreyer, Krishnaswami, Nanevski) [Project page]
CONCUR'13 Aspect-oriented linearizability proofs (with Henzinger, Sezgin)
ITP'13 Adjustable references [Project page]
TASE'13 A programming language approach to fault tolerance for fork-join parallelism (with Zengin) [Project page]
POPL'13 The power of parameterization in coinductive proof (with Hur, Neis, Dreyer) [Project page]
Tech.rep. The transitive composability of relation transition systems (with Hur, Neis, Dreyer) [Coq scripts]
JACM CompCertTSO: a verified compiler for relaxed-memory concurrency (with Sevcik, Zappa Nardelli, Jagannathan, Sewell) [Project page]
POPL'12 The marriage of bisimulations and Kripke logical relations (with Hur, Dreyer, Neis) [Technical appendix] [Coq scripts]

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

Valid XHTML 1.0 Strict Valid CSS!