A Systematic Approach to Probabilistic Pointer Analysis

Abstract. We present a formal framework for syntax directed probabilistic program analysis. Our focus is on probabilistic pointer analysis. We show how to obtain probabilistic points-to matrices and their relational counterparts in a systematic way via Probabilistic Abstract Interpretation (PAI). The analysis is based on a non-standard semantics for a simple imperative language which corresponds to a Discrete-Time Markov Chain (DTMC). The generator of this DTMC is constructed by composing (via tensor product) the probabilistic control flow of the program and the data updates of the different variables at individual program points. The dimensionality of the concrete semantics is in genhibitively large but abstraction (via PAI) allows for a drastic (exponential) reduction of size.

• Type: Conference
• Year: 2007
• Where: APLAS
• Authors: Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky
• Keywords: APLAS 2007, Probabilistic, Probabilistic Pointer Analysis, Probabilistic Program Analysis, Programming Languages