As networked systems become critical infrastructure, theirdesign must reflect their new societal role. Today, we build systemswith hundreds of heuristics but often do not understand their inherent and emergent behaviors. I will present a set of tools and techniques to prove performance properties of heuristics running in real-world conditions. Rigorous proofs can not only inspire confidence in our designs, but also give counter-intuitive insights about their performance.

A key theme in our approach is to model uncertainty in systems using non-random, non-deterministic objects that cover a wide range of possible behaviors under a single abstraction. Such models allow us to analyze complex system behaviors using automated reasoning techniques.

I will present automated tools to analyze congestion control and process scheduling algorithms. These tools prove performance properties and find counter-examples where widely deployed heuristics fail. I will also show that current end-to-end congestion control algorithms that bound delay cannot avoid starvation and present a method to beamform wireless signals using thousands of antennas.