This course introduces various methodologies for formal specification, testing and verification, to understand and eliminate bugs undermining system security. Two general methodologies are considered: dynamic methodologies using property-based testing and symbolic execution, and static methodologies involving program-based formal verification techniques.