 Formal verification methods require a representation of the software under verification. In theorem proving (see van Leeuwen 1990), programs are represented in terms of axiomatic systems and a set of rules of inference representing the pre- and post-conditions of program transitions. A proof of correctness is then obtained by deriving formulas expressing specifications from the axioms. In model checking (Baier and Katoen 2008), a program is represented in terms of a state transition system, its property specifications are formalised by temporal logic formulas (Kröger and Merz 2008), and a proof of correctness is achieved by a depth-first search algorithm that checks whether those formulas hold of the state transition system.