Probabilistic Abstract Interpretation of Imperative Programs using Truncated Normal Distributions