Teaching formal methods through Frama-C & SPARK

How can we educate future engineers about formal methods in few hours when they do not have a strong background in theoretical Computer Science? That is a challenge we are trying to take up at ISAE-SUPAERO in the critical systems architecture curriculum. We will present some feedback on what the students can learn and do in less than 15 hours and also present SPARK by Example, an adaptation of ACSL by Example mainly developed by two undergraduates in less than 3 months.