Model Checking

This course covers methods and tools for automatically checking whether a system (software or hardware) meets a given specification.

This course covers methods and tools for automatically checking whether a system (software or hardware) meets a given specification.

Course program

• The need for formal methods to verify hardware and software systems
• Reactive systems
• The model-checking process and its advantages
• System modeling (Kripke structure)
• Specification modeling (CTL and LTL temporal logics, fairness)
• Model-checking algorithms and their complexity
• Improvements: symbolic model-checking and on-the-fly model-checking
• Realistic examples