In particular, you will learn to model complex software systems and apply automated proof techniques to verify their correctness, thereby increasing trust in digital systems. Using the power of symbolic computation, the specialization teaches you how to tackle hard computational problems, as well as to realize reasoning for artificial intelligence. It also equips you with the detailed knowledge of concurrency required to analyze parallel systems, but also with knowledge about non-deterministic and probabilistic computational models. Finally, you will learn to harness the power of quantum computers, for solving problems more efficiently than with classical computers.