Este curso tem como objetivo discutir o estado da arte da verificação formal de programas sequenciais e concorrentes. Neste curso serão abordados os fundamentos de semântica de linguagens de programação e verificação de programas, assim como o processo de desenvolvimento e planejamento da verificação formal dentro do ciclo de vida do software.