Formal Verification

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.