PL/Verification @ MPI-SWS


UPMARC summer school slides

I am a tenure-track researcher at MPI-SWS. I got my BA (2004) and PhD (2008) from the University of Cambridge. Before joining MPI-SWS in October 2010, I was a postdoc 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 (2nd year PhD), Marko Doko (2nd year PhD)

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

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

Recent papers

DISC'15 Modular verification of concurrency-aware linearizability (with Hemed, Rinetzky)
Draft Lightweight verification of separate compilation (with Kang, Kim, Hur, Dreyer) [Project page]
CONCUR'15 Rely/guarantee reasoning for asynchronous programs (with Gavran, Niksic, Kanade, Majumdar)
ICALP'15 Owicki-Gries reasoning for weak memory models (with Lahav) [Project page]
JFP Mtac: A monad for typed tactic programming in Coq (with Ziliani, Dreyer, Krishnaswami, Nanevski) [Project page]
LMCS Aspect-oriented linearizability proofs (with Chakraborty, Henzinger, Sezgin)
ICFP'15 Pilsner: A compositionally verified compiler for a higher-order imperative language (with Neis, Hur, Kaiser, McLaughlin, Dreyer) [Project page]
ECOOP'15 Asynchronous liquid separation types (with Kloos, Majumdar) [Project page]
PLDI'15 Verifying read-copy-update in a logic for weak memory (with Tassarotti, Dreyer) [Project page]
PLDI'15 A formal C memory model supporting integer-pointer casts (with Kang, Hur, Mansky, Garbuzov, Zdancewic) [Project page]
CPP'15 Formal reasoning about the C11 weak memory model
CPP'15 Proving lock-freedom easily and automatically (with Jia, Li) [Project page]
POPL'15 Common compiler optimisations are invalid in the C11 memory model and what we can do about it (with Balabonski, Chakraborty, Morisset, Zappa Nardelli) [Project page]
OOPSLA'14 GPS: Navigating weak-memory with ghosts, protocols, and separation (with Turon, Dreyer) [Project page]
Automating the choices of consistency levels in replicated systems (with Li, Leitão, Clement, Preguiça, Rodrigues)
Tech.rep. A logical step forward in parametric bisimulations (with Hur, Neis, Dreyer) [Project page]

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

Valid XHTML 1.0 Strict Valid CSS!