Formal approaches to software testing

The process of testing software is an important technique for checking and validating the correctness of software. Unfortunately, it is usually difficult, expensive, time consuming and often error prone to achieve both an effective and efficient testing process. Formal methods are a method of specifying and verifying software systems using mathematical and logic approaches. This allows the analysis and reasoning of software systems with precision and rigor. Formal methods target the verification and the proving of correctness, while testing can only show the presence of errors. The use of formal methods can also automate the generation of test cases from formal specifications which can lead to less expensive and less error prone testing process.