Describes Woodpecker, a system that leverages path slicing to speed up symbolic execution. It enables users to check systems rules, and avoids checking program paths irrelevant to the rule, drastically reducing the amount of redundant work.

Describes a program analysis framework for analyzing multithreaded programs with high precision. The key idea is to statically analyze a multithreaded program toward only a small set of schedules to improve precision, then enforce these schedules at runtime for soundness.

Studies the security consequences of concurrency errors.

Describes Peregrine, a system for efficiently making threads deterministic, addressing a key open challenge within the field of deterministic execution.

Describes RacePro, a system for finding process races (e.g., multiple processes accessing a shared resource such as a file without proper synchronization).

Our latest model checking paper. It describes a new reduction technique that decomposes a full distributed system into components and then explores the executions of these components in a divide-and-conquer way.

Studies the security consequences of concurrency errors.

Argues that process races (e.g., multiple processes accessing a shared resource such as a file without proper synchronization) are bad and that the research community has not given them their due share of attention.

Presents a crucial problem in data-parallel computing: how to evenly partition data, and sketches a solution to this problem.

Describes CODE, a system for automatically detecting software configuration errors. The key insight is to infer configuration access invariants that predict what access events follow what contexts.

Describes Tern, a system for making threads more deterministic and stable. The key idea is to memoize past schedules and reuse them when possible, much like the natural tendencies in animals and humans to repeat familiar routes to avoid possible hazards along unknown routes.

Describes LOOM, a live-workaround system for fixing races in live applications. LOOM is safe (live-update will not introduce new errors), fast (negligible overhead for most benchmarks), and flexible (able to fix all bugs evaluated).

A more complete description of LOOM compared to our OSDI '10 paper.

Describes how we found many copy-and-paste bugs in a large commercial code base.

Describes how we applied our in-situ model checking approach to find 10 protocol-level errors in three real distributed systems, including a production system that has been managing more than 100 thousand machines for over two years. Note this version has two minor calculation errors fixed.

Describes a version of eXplode for in-vivo model checking.

Describes a distributed version of eXplode.

Describes our in-situ model checking approach, which made it easy to thoroughly check real systems. We applied eXplode to 17 storage systems and found serious data-loss errors in every system checked. This paper is my favorite in describing our model checking approach.

A journal version of our FiSC work, forwarded from OSDI 04.

Describes how we generated disks-of-death using symbolic execution. These disks, when mounted, can crash or take over control of your machine.

Describes a preliminary version of the eXplode storage system checker

Describes how we leveraged model checking to find serious errors in three widely used, well tested Linux file system errors. Some of these errors can vaporize your entire file systems.

Describes an extensible and lightweight annotation system that allows programmers to write a small set of domain-specific annotations to effectively annotate large bodies of code.

Presents our study of the errors found using meta-compilation. Some interesting conclusions include drivers are up to three to seven times buggier than the rest of the kernel.

Describes how we can exploit the correlations of error messages emitted by static analysis tools to cluster false positives together, thus improve the effectiveness of the static analysis tools.

Describes a new replica placement strategy that uses multiple linear hash functions to achieve high performance, scalability, and availability.