An advanced course on verification techniques for specifying and verifying programs. Cutting-edge formal methods, program analysis, theorem proving techniques will be discussed. Students with a good background in logic are encouraged to take this course.