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:
- propositional logic - syntax, proof methods, SAT solving
- first-order logic - syntax, proof rules, first-order theorem proving
- first-order theories - syntax, overview common ones, SMT solving
- deductive verification - hoare logic, verification conditions and tool (dafny)
- decision procedures - decision procedures for common first-order theories, combination of decision procedures