Papers

A New Approach to Proving the Correctness of Multiprocess Programs

 

A Distributed Algorithm for Minimum-Weight Spanning Trees

 

Using Time Instead of Timeout for Fault-Tolerant Distributed Systems

 

Reaching Agreement in the Presence of Faults

 

Model Checking TLA+ Specifications

 

Reliable Communication over Unreliable Channels

 

Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study

 

Optimal Time Self Stabilization in Dynamic Systems

 

Computation in networks of passively mobile finite-state sensors

 

Renaming in an asynchronous environment

 

What Good are Models and What Models are Good?