The course aims at providing a systematic account of computer science methods, formalisms, and algorithms for the formal specification and automatic verification/validation of complex reactive systems and their use in the areas of artificial intelligence and cybersecurity. A prominent role is assigned to the theory of automata operating on infinite objects (words and trees) and to temporal logics (LTL, CTL, CTL*, mu-calculus). A special attention is given to the expressive equivalence between classes of automata and logical systems. The possible role of the logical theory of games in formal verification is illustrated as well. From the algorithmic point of view, on the basis of the considered computational models and specification formalisms, the course studies in detail the main algorithms for specification consistency checking (satisfiability checking) and model checking. A special emphasis is given to model checking algorithms, that make it possible to validate the behaviour of hardware and software systems, modelled by means of a suitable mathematical model, e.g., an automaton, with respect to their formal requirements, specified by means of logical formulas, e.g., CTL formulas. In particular, the course described the main achievements in improving the performance of model checking algorithms (symbolic model checking, OBDD, partial order reduction). Moreover, a short account of meaningful examples of model checkers is given. In addition, some advanced topics are briefly introduced such as, for instance, the synthesis problem. In the last part of the course, we describe some applications of considered techniques and tools to automated planning and symbolic verification of cryptographic protocols.