My research interest is the use of the shared memory programming paradigm to program distributed, parallel, or concurrent or systems conveniently, efficiently, and correctly.

I am particularly interested in the following topics:

• Concurrent, Parallel, and Distributed Programming Models
  (see the Revisions project)
• Touch-enabled scripting languages for mobile+cloud
  (see the TouchDevelop project)
• Relaxed Memory Models, Eventual Consistency, and Consistency in Distributed Systems
  consider attending the LASER summer school 2013 in Elba! I will be presenting lectures on this topic.
• Verification and Debugging Tools for Concurrent Programs
  (see the Cuzz and CHESS projects)

Recent Publications

(A more verbose list showing all my coauthors is available here.)

• [PLDI'13] It's Alive! Continuous Feedback in UI Programming
• [TechReport 2013-39] Understanding Eventual Consistency
• [PLDI'12] Multicore Acceleration of Priority-Based Scheduler for Concurrency Bug Detection
• [ECOOP'12] Cloud Types for Eventual Consistency
• [ESOP'12] Eventually Consistent Transactions, full version available here
• [ESOP'12] What's Decidable About Weak Memory Models?
• [ESOP'12] Concurrent Library Correctness on the TSO Memory Model
• [OOPSLA'11] (Distinguished Paper Award) Two for the Price of One: A Model for Parallel and Incremental Computation
• [Haskell'11] Prettier Concurrency: Purely Functional Concurrent Revisions
• [WoDet'11] Roll Forward, Not Back: A Case for Deterministic Conflict Resolution
• [ESOP'11] Semantics of Concurrent Revisions, extended version available here
• [OOPSLA'10] Concurrent Programming with Revisions and Isolation Types
• [OSDI'10] Effective Data-Race Detection for the Kernel
• [PLDI'10] Line-Up: A Complete and Automatic Linearizability Checker
• [CC'10] Verifying Local Transformations of Concurrent Programs
• [ASPLOS'10] A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
• [POPL'10] On the Verification Problem for Weak Memory Models
• [PPoPP'10] GAMBIT: Effective Unit Testing for Concurrency Libraries
• [OOPSLA'09] The Design of a Task-Parallel Library
• [HotPar'09] Lightweight Software Transactions for Games
• [CAV'08] Effective Program Verification for Relaxed Memory Models
• [PLDI'07] CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models
• [CAV'06] Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study
• [VMCAI'05] Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement

Professional Activities

• Program Committee: POPL '13 (PC), PLDI '13 (ERC), ASPLOS '13 (ERC), OOPSLA '11 (PC)
• Lecturer at 2012 Summer School on Concurrency in St. Petersburg
• Dagstuhl Seminar on Multi-Core Memory Models and Concurrency Theory
• Dagstuhl Seminar on Consistency in Distributed Systems (Feb. 2013)
• 2013 LASER summer school in Elba