Formal verification of a program is the mathematical proof that it does what is expected of it. The 21st century has seen a vast worldwide interest in formal methods. Four journals (Automated Reasoning, Logic and Algebraic Programming, Formalized Mathematics, and Science of Computer Programming) and over a dozen yearly conferences, each of which has been held at least since 2000, are specifically devoted to these matters. Centers of ongoing formal methods research include Argonne, Berkeley, Bialystok (Poland), Cambridge, Clemson, HP, INRIA, Iowa State, Karlsruhe, Lausanne, Microsoft, MITRE, Munich, NYU, Penn, Praxis, and SRI. Methods have been developed for Java (JML), Ada (SPARC), C#, C, and Eiffel (Spec#), Haskell, Ocaml, and Scheme (Coq), Pascal (Sunrise), Modula-3 (ESC), and a number of special-purpose languages. This course is an introduction to this vast world of formal methods. Our concern will be the formal verification of the widest possible variety of programming language features and techniques. Each student will carry out an investigation of one or another of the existing formal verification systems, applying it to a program of the student's choice.