Abstract:<p><pre><code> > 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.</code></pre>