This course provides an introduction to the three main approaches for defining the semantics of programming languages (operational, denotational, and axiomatic). It then illustrates how they can be utilized to prove basic program properties such as safety and termination. Finally, it looks into LTL verification from a logic-game-automaton perspective.