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.