+++
title = "Design Trade-offs for the Scheduling Proof"
date = "2022-11-16"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3i"]
forwardlinks = ["3c3k"]
zettelid = "3c3j"
+++

There are a few trade-offs that were made during the scheduling proof,
such as:

-   deciding to use flat predicates instead of a tree-like structure
-   if-conversion, which is a more self-contained way to prove the
    translation without having to worry about the performance of the
    code
-   The representation of the predicates is also an interesting
    trade-off, because there are various ways to do this.
-   Using if-statements or constraints to prove the backwards simulation
    in the abstract interpretation.

**\*\***