In this talk, I will introduce the concept of a “monotonic theory” and demonstrate how such theories arise in many practical contexts, e.g., in connection with graph properties such as reachability, shortest paths and maximum flow. I will then outline how to build an SMT solver to support these monotonic theories and describe how we have used this solver to improve the state of the art in solving two prominent real-world application problems from circuit design and data centre operation: multi-layer escape routing for ball grid arrays and virtual data centre allocation.

Joint work with: Sam Bayless, Alan Hu and others.