Back to teaching

Formal Methods 2020

Course page

  1. nuXmv introduction27-03-2020

    00-course_information.pdf 01-nuxmv_introduction.pdf 01-adder.smv 01-adder_reset.smv

  2. nuXmv model checking03-04-2020

    02-nuxmv_mc.pdf 02-simple_mutex.smv 02-yet_another_mutex.smv 02-simple_ts.smv 02-bubblesort01.smv 02-bubblesort02.smv

  3. nuXmv finite state model checking exercises10-04-2020

    03-nuxmv_planning.pdf 03-examples.zip 03-exercises.zip

  4. Additional commands for finite state systems17-04-2020

    04-debug_fsm.pdf 04-examples.zip

  5. nuXmv BMC-based model checking24-04-2020

    05-nuxmv_bmc.pdf 05-in_class_cannibals.smv 05-exercises.zip

  6. nuXmv infinite state model checking07-05-2020

    06-nuxmv_infinite_state.pdf

  7. incremental inductive verification14-05-2020

    07-iiv.pdf

  8. liveness-to-safety, totalising transition relation22-05-2020

    08-l2s_and_totalisation.pdf 08-examples.zip

  9. nuXmv exercises28-05-2020

    09-nuxmv_exercises.pdf 09-exercises.zip

  10. nuXmv for timed systems29-05-2020

    10-nuxmv_timed_systems.pdf 10-examples.zip 10-exercises.zip

  11. HyCOMP04-06-2020

    11-hycomp_hybrid_systems.pdf 11-examples.zip 11-exercises.zip

  12. Exam-like exercises05-06-2020

    12-exam_simulation.pdf 12-solutions.zip