Static analysis of numeric program properties has a broad range of
useful applications. Such analyses can potentially detect array bounds
errors [1]}, analyze a program's resource
usage [2]}, [3]}, detect side
channels [4]}, [5]}, and discover vectors for denial of
service attacks [6]}, [7]}.
