John Rushby

A grouping.

What a regulator should accept as evidence, developed over sixteen years: formal methods and the certification of critical systems, partitioning in avionics architectures as the concrete case, just-in-time certification, and software verification and system assurance. The argument is about certification rather than proof -- of the corpus's three answers to whether formal methods pay, this is the one that treats the certifier as the audience.