同期アルゴリズム

私は携帯電話とPC用有償ソフトで同期をとってスケジュール管理をしているのですが、同期のアルゴリズムが「いまいち」で困ります。たまに一方で削除したスケジュールが復活したり、一方で変更したスケジュールが重複（変更前と変更後）したりすることがあるのです。そういう点でUnisonは極めてよくできていて、こういう微妙なアルゴリズムでは（仕様レベルの）形式的手法が本当に有用なのだなあ（詠嘆）、などと今更ながら身びいき抜きで感心してしまいました。Unisonの形式的仕様やCoqによる参照実装(!)の検証についてはここに論文やスライドがあります、と身内の宣伝。