Skip to main content
PRL Project

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.