Back to teaching

Formal Methods 2019

Credit for the material of the slides from 01 to 10 goes to previous years teaching assistants.

Course page

  1. Promela introduction15-03-2019

    00-course_information.pdf 01-promela_introduction.pdf 01-examples.zip

  2. Promela channels22-03-2019

    02-promela_channels.pdf 02-examples.zip 02-exercises.zip

  3. Spin LTL model checking29-03-2019

    03-spin_ltl_mc.pdf 03-examples.zip 03-leader_election_exercise.pml

  4. Spin exercises05-04-2019

    04-spin_exercises.pdf 04-exercises.zip

  5. nuXmv introduction12-04-2019

    05-nuxmv_introduction.pdf

  6. nuXmv model checking19-04-2019

    06-nuxmv_mc.pdf 06-exercises.zip

  7. Using model checkers to find plans03-05-2019

    07-nuxmv_planning.pdf 07-examples.zip 07-exercises.zip

  8. nuXmv BMC10-05-2019

    08-nuxmv_bmc.pdf

  9. nuXmv infinite state model checking17-05-2019

    09-nuxmv_infinite_state.pdf

  10. nuXmv, model checking timed systems21-05-2019

    11-nuxmv_timed_systems.pdf

  11. HyComp, hybrid model checker23-05-2019

    12-hycomp_hybrid_systems.pdf

  12. nuXmv exercises pt124-05-2019

    10-nuxmv_exercises.pdf 10-exercises.zip

  13. nuXmv exercises pt231-05-2019

    10-nuxmv_exercises.pdf 10-exercises.zip

  14. Exam-like exercises07-06-2019

    13-exam_simulation.pdf 13-exercises.zip