A gentle introduction to SMT-based program analysis
February 12, 2023 - Arnau Gàmez i Montolio
CC BY 4.0
This article offers a quick introduction to SMT-based program analysis. The goal is not to build or dive deep into the internal workings of an SMT solver. Rather, we want to explore how an SMT solver can be leveraged to reason about code properties in practice. Thus, for the most part, an SMT solver will be considered as a magic black-box that can answer a very simple question, as we will see shortly.