Many failures and vulnerabilities arise at the programming level. These are often due to inadequate handling of exceptional situations, poor understanding of the details of the programming language in use, and incomplete descriptions of the interfaces between components. This course aims to improve the practitioner's capability in writing and reviewing code, through a thorough understanding of static analysis, run- time assertion checking, and compile-time verification.