
An Introduction to Deductive Program Verification

This lecture introduces elementary concepts and techniques related to
deductive program verification, such as loop invariants, function
contracts, termination proofs, ghost code, modeling of data
structures, weakest preconditions, etc. A particular focus is made on
the use of automated theorem provers in the verification process and
the tension that may exists between an elegant specification and a
fully automated proof. The lecture includes many examples using the
Why3 tool (http://why3.lri.fr/) and lab sessions will invite
participants to formally verify small yet challenging programs using
Why3.



Contents

- ghost code: how to ensure non-interference and use in practice

- how to write a specification in the most elegant/efficient way

- the danger of inconsistency

- specifications that are wrong or too difficult to understand

- termination

