LFU:online

After completing this module, students can understand, create and correct the specifications of programs. They have acquired the skill to prove specifications formally. They use a combination of interactive and automatic methods to combine expressive logic with efficient search for proof.

• validation and verification
• partial correctness and termination
• automatic termination proofs
• working with an SMT-solver
• specification of program properties
• verification of functional programs
• verification of imperative programs
• proving techniques: induction, invariants, generalizations