This is an advanced graduate course on formal method foundations. The primary goal of this course is to provide students with an understanding of the basic concepts of formal methods, and their applications in computer science, especially in software modeling, computer security and program verification. Roughly, there are six board topics will be covered:

• Mathematical logic: propositional, first-order, and second-order
• Proof theory: including (semi-)automatic theorem proving and practical proof engineering
• Functional programming: especially the connection with logic via Curry-Howard isomorphism
• SAT and SMT: decision procedures
• Program modeling: Hoare logic, program verification

Prerequisite: basic discrete mathematics (sets, relations, functions, etc..). Some familiarity with functional programming is better, but not required.