There are many ways to use automated reasoning in the verification of computer systems. These range from heroic user guided proofs of correctness in powerful formal specification languages, to automatic checking of decidable properties in propositional logics.
I'll describe some traditional and some novel applications of theorem proving, taken from recent research at Cambridge, and then discuss a number of general issues that the examples raise.
