Although tests can reveal software errors, they cannot prove the absence of such errors. This calls for the concept of formal verification. If the behavior of a system can be described as a mathematical model, then the presence of a postulated correctness property can generally be verified or refuted mathematically using theorem proving or model checking. Although the use of these methods first appears very promising, exhausting their potential in practice proves extremely challenging.

Please contact us with any questions concerning formal specification and verification methods.