For each paper, by 12AM the evening before lecture:
What is the difference between data and control plane verification?
Why is minesweeper able to encode network routing computation as SMT constraints?
A video analytics application like “directional car counting” has the following DAG of modules: (Decode) à (Background subtraction) à (Compressed DNN) à (Heavyweight DNN) à (Custom logic for counting). If this video analytics query DAG were given to a big data systems stack (like Mesos or Yarn), can you come up with a simple example (and analogy) of a decision that would be made by: (i) the query optimizer, and (ii) the multi-resource scheduler?