This training dives into the world of symbolic model checking, a powerful technique for automatically verifying the correctness of software systems and hardware designs. Here’s what you will learn:

• Foundations of Automated Reasoning: Grasp the core concepts behind automated reasoning, a field dedicated to using logic and algorithms to prove properties about systems.
• Modeling Systems: Explore techniques for creating formal models that capture the behavior and functionality of a system under scrutiny. This could involve using state machines, transition systems, or other formalisms.
• Symbolic Representation: Learn how to represent sets of states and properties symbolically using techniques like Binary Decision Diagrams (BDDs). This allows for efficient manipulation of large state spaces encountered in complex systems.
• Formal Specification Languages: Get familiar with languages like CTL (Computation Tree Logic) for expressing properties you want to verify about your system model. These properties can encompass safety (no bad states) or liveness (desired events will eventually happen).
• Model Checking Techniques: Understand the core algorithms used in symbolic model checking. This might involve exploring symbolic search methods and techniques for efficiently checking if a system model satisfies the desired properties.
• Case Studies and Applications: The training likely incorporates examples of applying symbolic model checking to real-world problems. This could involve verifying properties of communication protocols, embedded systems, or even security protocols.