Periodic Reporting for period 4 - CoVeCe (Coinduction for Verification and Certification)

In critical application domains like aeronautics, distant surgerysystems, or cryptography, one needs to avoid bugs at all costs.Formal methods like verification provide automatic means of findingsome of these bugs. Certification, using proof assistants like Coq orIsabelle/HOL...