Converting Imperative Programs to Formulas

This lecture covers the process of converting imperative programs to formulas, focusing on verification-condition generation, formula construction, and expressing assignments and control flow structures as relations. It explains how to represent program correctness as a verification condition and implement it as an algorithm, using examples in Stainless. The lecture also discusses the translation of imperative statements, non-deterministic choices, and assumptions into formulas. Additionally, it explores the concepts of havoc, loop-free programs, and program paths, providing insights into constructing polynomial-sized formulas to describe program behaviors.