An introduction to verification using automated reasoning

Having software free of bugs is crucial for many areas, such as safety-critical systems or systems handling finances. Formal verification offers methods providing guarantees of program reliability or safety. To automatically verify such program properties, a common approach is to translate the property into a logical formula, and then employ automated reasoning tools to check if the formula holds. I will give an overview of how this approach works under the hood, and cover the basics of two directions in the field of automated reasoning: saturation-based theorem proving and SMT solving.