IO-automata and Ensemble
by Mark Bickford
I'll be talking about modeling Ensemble protocol layers with IO-automata and proving propoerties of them. I'll show a simplified version of the Total-Ordering layer and its invariants.
I'll also talk about how we try to automate, to some extent, the task of proving invariants of IO-automata using a meta-theorem.