Lecture

Converting Imperative Programs to Formulas

Description

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.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.