Formal program verification is an important approach to verifying safety and security of software systems. In this approach we define the semantics (i.e., the mathematical description of the behavior) of the program and specify programs' desirable properties, e.g., safety and security guarantees, in terms of their semantics. Program logics are formal mathematical tools (based on mathematical logic) which are used to establish that programs do indeed enjoy the aforementioned desirable properties. In this course, we will introduce the Iris program logic (https://www.iris-project.org) and discuss how it is used to specify and prove safety and security properties of software systems.