Z3: The Backbone of Modern Verification
SMT solvers are the engine behind many verification tools, translating logical formulas into concrete (un)satisfiability results. Understanding SMT solving is essential for appreciating the power and limitations of automated reasoning.
Z3 is one of the most widely used SMT solvers, developed by Microsoft Research. This seminar covers its architecture, core solving techniques, and theory support (e.g., arithmetic, arrays, quantifiers). We also look at how Z3 is integrated into tools like Dafny, Boogie, and Viper, and what makes it performant in practice. Participants will create and solve a range of small verification problems directly in Z3 to better understand its capabilities.