Probabilistic Abstract Interpretation of Imperative Programs using Truncated Normal Distributions

istic Abstract Interpretation of Imperative Programs using Truncated Normal Distributions Michael J. A. Smith1 ,2 Laboratory for Foundations of Computer Science University of Edinburgh Edinburgh, United Kingdom When modelling a complex system, such as one with distributed functionality, we need to choose an ape level of abstraction. When analysing quantitative properties of the system, this abstraction is typically probabilistic, since we introduce uncertainty about its state and therefore its behaviour. In parwhen we aggregate several concrete states into a single abstract state we would like to know the distribution over these states. In reality, any probability distribution may be possible, but this leads to an intractable analysis. Therefore, we must find a way to approximate these distributions in a safe manner. We present an abstract interpretation for a simple imperative language with message passing, where trunltivariate normal distributions are used as the abstraction. This a...

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Michael J. A. Smith
• Keywords: Abstract Interpretation, ENTCS 2008, Istic Abstract Interpretation, Normal Distributions