CpSc 513: Introduction Formal Verification -- Lecture notes

• September 8: Course Pitch
  • slides
  • all_aboard.py -- the SMT example from the slides
  • puzzle_utils.py -- A few handy functions for puzzle solving with Z3
• September 10:Course Overview (no reading)
• slides
• bf0.py: symbolic constraints for binary search -- brute force unwinding of the loop
• bf1.py: symbolic constraints for binary search -- same as bf0.py with the bug in the implementation of binary search fixed.
• search_invariant.py: verification using an invariant. Includes check for termination.
• September 15:Automatic Exploit Generation
• summary.html: my example of a paper summary
• September 17:Introduction to SMT Solvers
• September 22:Symbolic Program Execution -- current practice
• September 24:Symbolic Program Execution -- the “classic” paper
• September 29:SAT Solving -- the DPLL algorithm
• October 1:BDDs -- a canonical data structure for representing Boolean functions

The course will continue with model checking for hardware and software, applications to software verification, cyber physical systems, and VLSI circuits. We'll probably cover a few more verification techniques including abstraction methods and interpolants. Use cases from industry will be explored.