> Abstract—File synchronization services such as Dropbox are used by
    > hundreds of millions of people to replicate vital data. Yet formal
    > models of their behavior are lacking. We present the first
    > formal—and testable—model of the core behavior of a modern file
    > synchronizer, and we use it to discover surprising behavior in two
    > widely deployed synchronizers. Our model is based on a technique for
    > testing nondeterministic systems that avoids requiring that the
    > system’s internal choices be made visible to the testing framework.