Formal Methods 2020

Most of the content of the slides has been taken from previous years slides.

All registrations will be uploaded here

1. nuXmv introduction: 27-03-2020
   • 00-course_information.pdf
   • 01-nuxmv_introduction.pdf
   • 01-adder.smv
   • 01-adder_reset.smv
2. nuXmv model checking: 03-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 exercises: 10-04-2020
   • 03-nuxmv_planning.pdf
   • 03-examples.zip
   • 03-exercises.zip
4. Additional commands for finite state systems: 17-04-2020
   • 04-debug_fsm.pdf
   • 04-examples.zip
5. nuXmv BMC-based model checking: 24-04-2020
   • 05-nuxmv_bmc.pdf
   • 05-in_class_cannibals.smv
   • 05-exercises.zip
6. nuXmv infinite state model checking: 07-05-2020
   • 06-nuxmv_infinite_state.pdf
7. incremental inductive verification: 14-05-2020
   • 07-iiv.pdf
8. liveness-to-safety, totalising transition relation: 22-05-2020
   • 08-l2s_and_totalisation.pdf
   • 08-examples.zip
9. nuXmv exercises: 28-05-2020
   • 09-nuxmv_exercises.pdf
   • 09-exercises.zip
10. nuXmv for timed systems: 29-05-2020
    • 10-nuxmv_timed_systems.pdf
    • 10-examples.zip
    • 10-exercises.zip
11. HyCOMP: 04-06-2020
    • 11-hycomp_hybrid_systems.pdf
    • 11-examples.zip
    • 11-exercises.zip
12. Exam-like exercises: 05-06-2020
    • 12-exam_simulation.pdf
    • 12-solutions.zip