In the computer science community, the term Formal Methods denotes the use of mathematical methods, in particular those of mathematical logic and universal algebra, in the specification and verification of computational systems. (Here, the term verification means a formal mathematical proof that an implementation of a system fulfils its formal specification. Such proofs can be very hard and are almost always complicated. Therefore, formal verification is not without its detractors!) Formal methods in current industrial practice usually means the use of precise languages with a precise semantics to specify system behavior. It is undeniable that the use of formal methods aids precision. What is normally questioned is the actual cost/benefit ratio of using a particular formal method in a particular project. There is also common acknowledgement that developing formal methods, including verification, is a hard research area. Research in Formal Methods has led to Turing awards (the `Nobel prize' of computer science) for Britons Tony Hoare and Robin Milner, the Dutchman Edsger Dijkstra, and the Americans Robert Floyd, Dana Scott and John Hopcroft; and the 1991 Current Prize of the American Mathematical Society Prize in Automated Theorem Proving for US computer scientists Robert Boyer and J. Strother Moore.