In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
This is what we are doing in SE212.
Formal verification (FV) is based on logical reasoning.
Formal verification means using logical reasoning to check the correctness of a program for all possible inputs.
- However, these methods can require more effort, and therefore are complementary to testing and inspection.
Verification helps reduce bugs in code and reduces the debugging and maintenance tasks (time and cost)
For safety-critical software, we can’t tolerate the presence of any bugs in the software
- So I think for example in the Aviation industry
Software can have a very long lifetime. Documentation is necessary for communication in multi-person, multi-year software development projects. Good documentation facilitates code re-use. Formal specification is a precise and concise way to write this documentation.