formal verification - prove or disprove correctness of system w.r.t. to a specification

diff between testing:

  • formal verification always correct, no bugs with unlimited test cases
  • testing impossible to do this, it finds bugs with limited test cases

examples:

  • verify program has no nullptr deference for any input
  • verify output of sort algo always sorted

why learn:

  • useful in many research areas (programming language, system)
  • applied in many industry, big-tech

methods of formal verification:

  • deductive verification - course focus on this
  • model checking
  • abstract interpretation
  • type systems

overview:

  1. propositional logic - syntax, proof methods, SAT solving
  2. first-order logic - syntax, proof rules, first-order theorem proving
  3. first-order theories - syntax, overview common ones, SMT solving
  4. deductive verification - hoare logic, verification conditions and tool (dafny)
  5. decision procedures - decision procedures for common first-order theories, combination of decision procedures