This course tries to bridge the gap between the formal definition and practical use of Mathematical Tools in Computer Science.

• Propositional and predicate logic using Coq

• Inductive proofs using Coq

• Hoare logic using Why3