IO-automata & Ensemble
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.