Model checking has been on my list of “stuff to understand” for a long time. It’s one of the few ‘formal methods’ which gets noticeable positive press. This month’s Communications of the ACM had a big article about it, of which I understood very little. However, it prompted me to search t’internet and this introduction to model checking which, shockingly, has an actual worked (ableit trivial) example. Now I am enlightened!