Automatic verification of requirement specifications

Use of formal specification does not a priori guarantee correctness. So far a number of animation approaches have been used for validating formal specification correctness. However, they require complex validation procedures and exhaustive testing and have some intrinsic limitations. On the other hand, formal specification can be validated by showing that certain properties are logical consequences of the specification, which is called formal reasoning or verification. Tool support, in particular an automated theorem prover, is needed for this task. We discuss some experiences in formal specification validation with the automated theorem prover