See also:
[By subject]
[DBLP]
[GoogleScholar]
### PhD dissertation

### Journal articles

### Conference papers (peer-reviewed)

### Invited papers and technical reports

**Modular fine-grained concurrency verification.**

University of Cambridge, July 2007.

Also published as technical report UCAM-CL-TR-726, University of Cambridge Computer Laboratory, July 2008.

[TR version]

**Persistency semantics of the Intel-x86 architecture.**

Proc. ACM Program. Lang. 4, POPL, Article 11 (January 2020)

[Paper] [@ACM] [More...]**Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models.**

Proc. ACM Program. Lang. 3, OOPSLA, Article 137 (October 2019)

[Paper] [@ACM] [More...]-
**Effective lock handling in stateless model checking.**

Proc. ACM Program. Lang. 3, OOPSLA, Article 173 (October 2019)

[Paper] [@ACM] [More...] -
**On library correctness under weak memory consistency**

Proc. ACM Program. Lang. 3, POPL, Article 68 (January 2019)

[Paper] [@ACM] [More...] -
**Bridging the gap between programming languages and hardware weak memory models.**

Proc. ACM Program. Lang. 3, POPL, Article 69 (January 2019)

[Paper] [@ACM] [@arXiv] [More...] **Grounding thin-air reads with event structures.**

Proc. ACM Program. Lang. 3, POPL, Article 70 (January 2019)

[Paper] [@ACM] [More...]**Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model.**

Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (November 2018)

[Paper] [@ACM] [More...]-
**Effective stateless model checking for C/C++ concurrency.**

Proc. ACM Program. Lang. 2, POPL, Article 17 (January 2018)

[Paper] [@ACM] [More...] **Geo-Replication: Fast If Possible, Consistent If Necessary.**

IEEE Data Engineering Bulletin 39(1): 81-92 (March 2016)

[@IEEE]**Mtac: A monad for typed tactic programming in Coq.**

J. Functional Programming 25 (August 2015)

[Paper] [@CUP] [More...]**Aspect-oriented linearizability proofs.**

Logical Methods in Computer Science 11(1:20) (March 2015)

[@LMCS]**CompCertTSO: A verified compiler for relaxed-memory concurrency.**

J. ACM. 60(3):22 (June 2013)

[Paper] [@ACM] [More...]**Acute: High-level programming language design for distributed computation.**

J. Functional Programming 17(4-5): 547-612 (2007)

[Paper] [@CUP] [More...]

**HMC: Model checking for hardware memory models.**

In ASPLOS 2020 (March 2020)

[Paper]**Model checking for weakly consistent libraries.**

In PLDI 2019 (June 2019)

[Paper] [@ACM] [More...]**On the semantics of snapshot isolation.**

In VMCAI 2019 (January 2019)

[@arXiv] [@Springer]**On parallel snapshot isolation and release/acquire consistency.**

In ESOP 2018. LNCS 10801, pp. 940-967. Springer (April 2018)

[Paper] [@Springer] [More...]**A separation logic for a promising semantics.**

In ESOP 2018. LNCS 10801, pp. 357-384. Springer (April 2018)

[Paper] [@Springer] [Technical appendix] [More...]**Strong logic for weak memory: Reasoning about release-acquire consistency in Iris.**

In ECOOP 2017, pp. 17:1-17:29 (June 2017)

Best paper award at ECOOP'17

[Paper] [@LIPIcs] [More...]**Promising compilation to ARMv8 POP.**

In ECOOP 2017, pp. 22:1-22:28 (June 2017)

[Paper] [@LIPIcs]**Repairing sequential consistency in C/C++11.**

In PLDI 2017, pp. 618-632. ACM (June 2017)

Distinguished paper award at PLDI'17

[Paper] [@ACM] [More...]**Tackling real-life relaxed concurrency with FSL++.**

In ESOP 2017. LNCS 10201, pp. 448-475. Springer (April 2017)

[Paper] [@Springer] [More...]**Formalizing the concurrency semantics of an LLVM fragment.**

In CGO 2017, pp. 100-110. ACM (February 2017)

[Paper] [@ACM] [More...]-
**A promising semantics for relaxed-memory concurrency.**

In POPL 2017, pp. 175-189. ACM (January 2017)

[Paper] [@ACM] [More...] **Explaining relaxed memory models with program transformations.**

In FM 2016. LNCS 9995, pp. 479-495. Springer (November 2016)

[Paper] [@Springer] [More...]-
**Validating optimizations of concurrent C/C++ programs.**

In CGO 2016, pp. 216-226. ACM (March 2016)

[Paper] [@ACM] [More...] **Reasoning about fences and relaxed atomics.**

In PDP 2016, pp. 520-527. IEEE (February 2016)

[Paper] [@IEEE]-
**Taming release-acquire consistency.**

In POPL 2016, pp. 649-662. ACM (January 2016)

[Paper] [@ACM] [More...] -
**Lightweight verification of separate compilation.**

In POPL 2016, pp. 178-190. ACM (January 2016)

[Paper] [@ACM] [More...] **A program logic for C11 memory fences.**

In VMCAI 2016, LNCS 9583, pp. 413-430. Springer (January 2016)

[Paper] [@Springer] [More...]**Modular verification of concurrency-aware linearizability.**

In DISC 2015, pp. 371-387 (October 2015)

[Paper] [@Springer]**Pilsner: A compositionally verified compiler for a higher-order imperative language.**

In ICFP 2015, pp. 166-178 (September 2015)

[Paper] [More...]**Rely/guarantee reasoning for asynchronous programs.**

In CONCUR 2015, pp. 483-496 (September 2015)

[Paper] [@LIPIcs]**Asynchronous liquid separation types.**

In ECOOP 2015, pp. 396-420 (July 2015)

[Paper] [@LIPIcs] [More...]**Owicki-Gries reasoning for weak memory models.**

In ICALP 2015, Track B. LNCS 9135, pp. 311-323. Springer (July 2015)

[Paper] [@Springer] [More...]**Verifying read-copy-update in a logic for weak memory.**

In PLDI 2015, pp. 110-120, ACM (June 2015)

[Paper] [@ACM] [More...]-
**A formal C memory model supporting integer-pointer casts.**

In PLDI 2015, pp. 326-335. ACM (June 2015)

[Paper] [@ACM] [More...] -
**Common compiler optimisations are invalid in the C11 memory model and what we can do about it.**

In POPL 2015, pp. 209-220. ACM (January 2015)

[Paper] [@ACM] [More...] **Proving lock-freedom easily and automatically.**

In CPP 2015, pp. 119-127. ACM (January 2015)

[Paper] [@ACM] [More...]-
**GPS: Navigating weak memory with ghosts, protocols, and separation.**

In OOPSLA 2014, pp. 691-707. ACM (October 2014)

[Paper] [@ACM] [More...] **Automating the choices of consistency levels in replicated systems.**

In USENIX ATC 2014, pp. 281-292. USENIX (June 2014)

[Paper] [@USENIX]**Relaxed separation logic: A program logic for C11 concurrency.**

In OOPSLA 2013, pp. 867-884. ACM (October 2013)

[Paper] [@ACM] [More...]**Mtac: A monad for typed tactic programming in Coq.**

In ICFP 2013, pp. 87-100. ACM (September 2013)

[Paper] [@ACM] [Implementation (Mtac)]**Aspect-oriented linearizability proofs.**

In CONCUR 2013. LNCS 8052, pp. 242-256. Springer (August 2013)

[Paper] [@Springer]**Adjustable references.**

In ITP 2013. LNCS 7998, pp. 328-337. Springer (July 2013)

[Paper] [@Springer] [More...]**A programming language approach to fault tolerance for fork-join parallelism.**

In TASE 2013, pp. 105-112. IEEE (July 2013)

[Paper] [@IEEE] [More...]**The power of parameterization in coinductive proof.**

In POPL 2013, pp. 193-206. ACM (January 2013)

[Paper] [@ACM] [Coq library (Paco)]**The marriage of bisimulations and Kripke logical relations.**

In POPL 2012, pp. 59-72. ACM (January 2012)

[Paper] [@ACM] [More...]**Verifying fence elimination optimisations.**

In SAS 2011. LNCS 6887, pp. 146-162. Springer (September 2011)

[Paper] [@Springer] [More...]**Concurrent separation logic and operational semantics.**

In MFPS 2011. ENTCS 276, pp. 335-351. Elsevier (September 2011)

[Paper] [@Elsevier] [More...]**Separation logic in the presence of garbage collection.**

In LICS 2011, pp. 247-256. IEEE (June 2011)

[Paper] [@IEEE] [Technical appendix]**Relaxed-memory concurrency and verified compilation.**

In POPL 2011, pp. 43-54. ACM (January 2011)

[Paper] [@ACM] [More...]**Automatically proving linearizability.**

In CAV 2010. LNCS 6174, pp. 450-464. Springer (July 2010)

[Paper] [@Springer] [Technical report] [Tool (Cave)]**Concurrent abstract predicates.**

In ECOOP 2010. LNCS 6183, pp. 504-528. Springer (June 2010)

[Paper] [@Springer] [Technical report]**RGSep action inference.**

In VMCAI 2010. LNCS 5944, pp. 345-361. Springer (January 2010)

[Paper] [@Springer] [Tool (Cave)]**Structuring the verification of heap-manipulating programs.**

In POPL 2010, pp. 261-273. ACM (January 2010)

[Paper] [@ACM] [Proof scripts]**Bi-abductive resource invariant synthesis.**

In APLAS 2009. LNCS 5904, pp. 259-274. Springer (December 2009)

[Paper] [@Springer]**Finding heap-bounds for hardware synthesis.**

In FMCAD 2009, pp. 205-212. IEEE (November 2009)

[Paper] [@IEEE]**Deny-guarantee reasoning.**

In ESOP 2009. LNCS 5502, pp. 363-377. Springer (March 2009)

[Paper] [@Springer] [Technical report]**Proving that nonblocking algorithms don't block.**

In POPL 2009, pp. 16-28. ACM (January 2009)

[Paper] [@ACM]**Shape-value abstraction for verifying linearizability.**

In VMCAI 2009. LNCS 5403, pp. 335-348. Springer (January 2009)

[Paper] [@Springer] [Tool (Cave)]**A marriage of rely/guarantee and separation logic.**

In CONCUR 2007. LNCS 4703, pp. 256-271. Springer (September 2007)

[Paper] [@Springer] [Technical report] [More...]**Modular safety checking for fine-grained concurrency.**

In SAS 2007. LNCS 4634, pp. 233-238. Springer (August 2007)

[Paper] [@Springer] [Tool (SmallfootRG)]**Proving correctness of highly-concurrent linearisable objects.**

In PPoPP 2006, pp. 129-136. ACM (March 2006)

[Paper] [@ACM] [Technical report]**Acute: High-level programming language design for distributed computation.**

In ICFP 2005, pp. 15-26. ACM (September 2005)

[Paper] [@ACM] [More...]

**Program verification under weak memory consistency using separation logic.**

In CAV (1) 2017. LNCS 10426, pp. 30-46. Springer (July 2017)

[Paper] [@Springer]**Formal reasoning about the C11 weak memory model.**

In CPP 2015, pp. 1-2. ACM (January 2015)

[Paper] [@ACM] [Slides]**A logical step forward in parametric bisimulations.**

Technical report MPI-SWS-2014-003 (January 2014)

[Paper] [Project page with Coq scripts]**The transitive composability of relation transition systems.**

Technical report MPI-SWS-2012-002 (April 2012)

[Paper] [Coq scripts]