Abstract
This paper presents a formal specification for the unoptimized version of our algorithm presented in Section 4 of 4 and proves its safety (but not its liveness.) The specification uses the I/O automaton formalism of Tuttle an Lynch 8 and the proof is based on invariant assertions and simulation relations
Users
Please
log in to take part in the discussion (add own reviews or comments).