Ensuring the correctness of software is both difficult and important. While the problem is undecidable in general, there is a wide range of algorithms and techniques for solving it in many practical cases. In this course we will learn how the correctness of software can be mathematically proven using automated tools called solvers. We will explore some of the algorithms these tools rely on, and also gain hands-on experience in using them. We will focus on: Boolean satisfiability (SAT) solvers, Satisfiability Modulo Theories (SMT) solvers, and Linear Programming (LP) solvers, and their applications in analyzing software through deductive reasoning, symbolic execution, and model checking. We will also learn about applying these techniques, both theoretically and practically, to ensure the correctness of software generated through machine learning.