+ M2 Internship. Working on reproducibility and transparency of
+ assertions in the synchronous hybrid language
+ Zélus.
+ Definition of a formal semantics for a multi-solver language
+ back-end.
+
M1 Internship. Added support for case analysis and proofs by
- induction on inductive predicates in the Why3 framework.
+ induction on inductive predicates in the
+ Why3 framework.
Translated a Coq proof to Why3 as a test.