This is a hands-on course that teaches you how to prove that programs are correct. You will get in-depth experience with tools for this task, as well as an understanding of the theory behind them. This course thus equips you to pursue a career in writing safety-critical systems, or in pursuing higher studies in this area.