*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] new AFP entries*From*: Gerwin Klein <gerwin.klein at nicta.com.au>*Date*: Wed, 15 Mar 2006 08:52:39 +1100*Organization*: NICTA*Reply-to*: gerwin.klein at nicta.com.au*User-agent*: KMail/1.6.2

We are pleased to announce two new entires in the Archive of Formal Proofs [http://afp.sf.net]: Benjamin Porter: Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality [http://afp.sf.net/entries/ClockSynchInst.shtml] Abstract: This document presents the mechanised proofs of two popular theorems attributed to Augustin Louis Cauchy - Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality. and Damián Barsotti: Instances of Schneider's generalized protocol of clock synchronization. [http://afp.sf.net/entries/ClockSynchInst.shtml] Abstract: F. B. Schneider ("Understanding protocols for Byzantine clock synchronization'') generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. In Schneider's schema, each processor maintains a local clock by periodically adjusting each value to one computed by a convergence function applied to the readings of all the clocks. Then, correctness of an algorithm, i.e. that the readings of two clocks at any time are within a fixed bound of each other, is based upon some conditions on the convergence function. To prove that a particular clock synchronization algorithm is correct it suffices to show that the convergence function used by the algorithm meets Schneider's conditions. Using the theorem prover Isabelle, we formalize the proofs that the convergence functions of two algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch , meet Schneider's conditions. Furthermore, we experiment on handling some parts of the proofs with fully automatic tools like ICS and CVC-lite. These theories are part of a joint work with Alwen Tiu and Leonor P. Nieto "Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools'' in proceedings of AVOCS 2005 (http://users.rsise.anu.edu.au/~tiu/clocksync.pdf). In this work the correctness of Schneider schema was also verified using Isabelle (available at http://afp.sourceforge.net/entries/GenClock.shtml). Cheers, Gerwin

- Previous by Date: [isabelle] Nonlinear arithmetic for real numbers
- Next by Date: [isabelle] ax_specification parse error
- Previous by Thread: Re: [isabelle] Nonlinear arithmetic for real numbers
- Next by Thread: [isabelle] ax_specification parse error
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list