Lab 1

The first laboratory assignment is about using the WP plugin of Frama-C to formally verify one or two C programs (tabs.c, tabs_loop.c) controlling an anti-lock braking system (ABS) of a car.

The assignment is to be carried out individually or in a team of two students. It is due at the lab reporting session on September 20. Please have a printed and stapled lab report ready at the beginning of your reporting slot; it will be used as a basis for the evaluation.