After completing this courses students will understand what it means to
write rigorous descriptions of implementations and specifications of programs, verify programs, i.e. prove that the implementation of a program meets its specification, and synthesise programs, i.e. to derive a correct program from a given specification.
The course will contain the following topics: logical proofs, specification and correctness of programs, weakest preconditions, invariants, partial correctness, termination proofs, total correctness, and program synthesis.