********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle Verdier * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 5 mai 2000 **** 14h00 ********************************** rel^ache *** Vendredi 12 mai 2000 **** 14h00 ********************************* Leslie LAMPORT (Compaq Corporate Research) I. Distributed State Machines and Disk Paxos The state-machine approach to designing a fault-tolerant distributed system is reviewed. Disk Paxos, a new algorithm for implementing this approach, is described. It achieves fault-tolerance by replicating disks rather than processors. II. Disk Paxos in TLA+ The TLA+ specification language is introduced by writing a formal specification of the consensus protocol required by the state-machine approach. The TLA+ specification of the Disk Paxos consensus algorithm is then sketched, and a road map given for its correctness proof. The TLC model checker is then briefly described. *** Vendredi 19 mai 2000 **** 14h00 ********************************* Pas de se'minaire, salle Verdier occupe'e. No seminar, room Verdier not available. *** Vendredi 26 mai 2000 **** 14h00 ********************************* rel^ache ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************