Verification of Clock Synchronization Algorithms: Experiments on a Combination of Deductive Tools