Weak consistency semantics:

WMC verification:

SC verification:

Verified compilation:

Other topics:

Items with a check mark () come with a
mechanized proof in either Coq or Isabelle/HOL.

See also: [Publications chronologically] [DBLP] [GoogleScholar]

See also: [Publications chronologically] [DBLP] [GoogleScholar]

- Making weak memory models fair.

Proc. ACM Program. Lang. 5, OOPSLA, Article 98 (October 2021)

Distinguished paper award at OOPSLA'21

[Paper] [@ACM] [@arXiv] [Artifact @Zenodo] - Reconciling event structures with modern multiprocessors.

In ECOOP 2020. LIPIcs 166, pp. 5:1-5:26 (June 2020)

[Paper] [@Dagstuhl] [@arXiV] - Promising 2.0: Global optimizations in relaxed memory concurrency.

In PLDI 2020, pp. 362–376. ACM (June 2020)

[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...] - 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...] - 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...] - Taming release-acquire consistency.

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

[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...]

- The challenges of weak persistency.

In CALCO 2021. LIPIcs 211, pp. 4:1–4:3 (September 2021)

[Paper] [@Dagstuhl] - PerSeVerE: Persistency semantics for verification under ext4.

Proc. ACM Program. Lang. 5, POPL, Article 43 (January 2021)

[Paper] [@ACM] [More...] - 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...] - On the semantics of snapshot isolation.

In VMCAI 2019 (January 2019)

[@arXiv] [@Springer] - 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...] - On parallel snapshot isolation and release/acquire consistency.

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

[Paper] [@Springer] [More...]

- Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86.

Proc. ACM Program. Lang. 4, OOPSLA, Article 151 (November 2020)

[Paper] [@ACM] [More...] - A separation logic for a promising semantics.

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

[Paper] [@Springer] [Technical appendix] [More...] - Program verification under weak memory consistency using separation logic.

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

[Paper] [@Springer] - 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...] - Tackling real-life relaxed concurrency with FSL++.

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

[Paper] [@Springer] [More...] - Reasoning about fences and relaxed atomics.

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

[Paper] [@IEEE] - A program logic for C11 memory fences.

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

[Paper] [@Springer] [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...] - Formal reasoning about the C11 weak memory model.

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

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

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

[Paper] [@ACM] [More...] - Relaxed separation logic: A program logic for C11 concurrency.

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

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

- Truly stateless, optimal dynamic partial order reduction.

Proc. ACM Program. Lang. 6, POPL, Article 49 (January 2022)

[Paper] [@ACM] [Artifact @Zenodo] - Extending Intel-x86 consistency and persistency: Formalising the semantics of Intel-x86 memory types and non-temporal stores.

Proc. ACM Program. Lang. 6, POPL, Article 22 (January 2022)

[Paper] [@ACM] [Artifact @Inria] - Dynamic partial order reductions for spinloops.

In FMCAD 2021 (October 2021)

[Paper] [@IEEE] [More...] - GenMC: A model checker for weak memory models.

In CAV 2021 (July 2021)

[Paper] [@Springer] [Artifact @Zenodo] [More...] - BAM: Efficient model checking for barriers.

In NETYS 2021 (May 2021)

[Paper] - Verifying and optimizing the HMCS lock for Arm servers.

In NETYS 2021 (May 2021)

[Paper] - VSync: Push-button verification and optimization for synchronization primitives on weak memory.

In ASPLOS 2021, pp. 530-545. ACM (April 2021)

Distinguished paper award at ASPLOS'21

[Paper] [@ACM] - The decidability of verification under PS 2.0.

In ESOP 2021. LNCS 12648, pp. 1-29. Springer (March 2021)

[Paper] [@Springer] - HMC: Model checking for hardware memory models.

In ASPLOS 2020 (March 2020)

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

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

[Paper] [@ACM] [More...] - Model checking for weakly consistent libraries.

In PLDI 2019, pp. 96-110. ACM (June 2019)

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

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

[Paper] [@ACM] [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] - 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] - Deny-guarantee reasoning.

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

[Paper] [@Springer] [Technical report] - A marriage of rely/guarantee and separation logic.

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

[Paper] [@Springer] [Technical report] [More...] - Proving correctness of highly-concurrent linearisable objects.

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

[Paper] [@ACM] [Technical report]

- 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...] - Aspect-oriented linearizability proofs.

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

[@LMCS] - Proving lock-freedom easily and automatically.

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

[Paper] [@ACM] [More...] - Aspect-oriented linearizability proofs.

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

[Paper] [@Springer] - Automatically proving linearizability.

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

[Paper] [@Springer] [Technical report] [Tool (Cave)] - Bi-abductive resource invariant synthesis.

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

[Paper] [@Springer] - 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)] - Modular safety checking for fine-grained concurrency.

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

[Paper] [@Springer] [Tool (SmallfootRG)]

- Lightweight verification of separate compilation.

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

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

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

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

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

[Paper] [@ACM] [More...] - The marriage of bisimulations and Kripke logical relations.

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

[Paper] [@ACM] [More...] - 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]

- CompCertTSO: A verified compiler for relaxed-memory concurrency.

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

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

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

[Paper] [@Springer] [More...] - Relaxed-memory concurrency and verified compilation.

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

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

- Mtac: A monad for typed tactic programming in Coq.

J. Functional Programming 25 (August 2015)

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

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

[Paper] [@ACM] [Implementation (Mtac)] - Adjustable references.

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

[Paper] [@Springer] [More...] - The power of parameterization in coinductive proof.

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

[Paper] [@ACM] [Coq library (Paco)]

- Geo-Replication: Fast If Possible, Consistent If Necessary.

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

[@IEEE] - Modular verification of concurrency-aware linearizability.

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

[Paper] [@Springer] - Automating the choices of consistency levels in replicated systems.

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

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

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

[Paper] [@IEEE] [More...] - Finding heap-bounds for hardware synthesis.

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

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

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

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

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

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