Automated Reasoning: Symbolic Model Checking

This course introduces symbolic model checking, a powerful technique used to automatically verify whether software systems and programs satisfy specific properties. You will learn how complex systems can be represented as transition systems, how logical properties are expressed using Computation Tree Logic (CTL), and how symbolic methods help analyse large state spaces efficiently. 

What you will learn:

• Fundamentals of automated reasoning and model checking.  
• Representation of systems using states and transitions.  
• Application of Computation Tree Logic (CTL) to specify and verify system properties.  
• Principles and algorithms of Binary Decision Diagrams (BDDs).  
• Techniques for symbolic verification of large and complex systems.  
• Methods for automatically checking correctness and reachability properties in software and hardware systems. 

Follow the ‘go to course’ and sign up!