> I challenge you to write a program that will run a detailed mathematical model of a computer program... Model checking is well-established in hardware design

> I challenge you to write a program that will run a detailed mathematical model of a computer program... Model checking is well-established in hardware design and is making headway into software. Model checkers can verify high-level properties. For example, I am currently working on a p2p gossip algorithm. I use a probabilistic model checker to verify that the peer selection service provided by this algorithm fulfils its contract - in the steady state selected peers are uniformly distributed over the members of the network. I use a model checker because the maths involved is sufficiently complicated that I don't trust either my theoretical results or that the code matches the mathematical model I am working with.