Formal Software Verification

Verificação Formal de Software

English. Lecture notes for a master's course on proving properties of imperative programs in Lean. The course runs from classical logic and structured proofs, through functional programming, inductive predicates, and big-step operational semantics, to Hoare logic and automated verification with the mvcgen tactic. Every piece of Lean code in the notes is checked by the compiler when the site is built.

Português. Notas de aula de uma disciplina de mestrado sobre prova de propriedades de programas imperativos em Lean. A disciplina vai da lógica clássica e das provas estruturadas, passando por programação funcional, predicados indutivos e semântica operacional big-step, até a lógica de Hoare e a verificação automatizada com a tática mvcgen. O compilador checa todo o código Lean das notas na construção do site.