Tool support for formal methods

The author discusses the state of the art of formal methods tool support. The focus is on a particular tool: the EVES verification system. EVES is a new formal methods tool that integrates techniques from, among others, language design, language semantics, and logic and automated deduction. EVES demonstrates a number of the features that can be found in the state-of-the-art formal methods tool. The author gives brief introductions to various other formal methods tools (e.g., HOL, EHDM, the Boyer-Moore theorem prover) and discusses how these tools are being applied