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 verifica todo o
código Lean das notas na construção do site.