Formal Software Verification🔗

These are the lecture notes for the course Formal Software Verification, offered in the Master's program in Systems and Computing at the Military Institute of Engineering (IME), Rio de Janeiro.

The course presents the foundations and the corresponding infrastructure in Lean needed to prove properties of imperative programs by means of Hoare logic. It covers classical first-order logic with structured proofs, dependent type theory, interactive proving with forward and backward reasoning, functional programming and inductive types, structural induction, inductive predicates and rule induction, programming with effects and monads, big-step operational semantics of an imperative language, Hoare logic, and practical verification with the mvcgen tactic.

The main references are How To Prove It with Lean (HTPIwL), The Hitchhiker's Guide to Logical Verification (LoVe), and The Lean Language Reference.