On Probabilistic Techniques for Data Flow Analysis |
| |
Authors: | Alessandra Di Pierro Chris Hankin Herbert Wiklicky |
| |
Affiliation: | aDepartment of Computing, Imperial College London, 180 Queen's Gate, London SW7 2AZ, United Kingdom |
| |
Abstract: | We present a semantics-based technique for analysing probabilistic properties of imperative programs. This consists in a probabilistic version of classical data flow analysis. We apply this technique to pWhile programs, i.e programs written in a probabilistic version of a simple While language. As a first step we introduce a syntax based definition of a linear operator semantics (LOS) which is equivalent to the standard structural operational semantics of While. The LOS of a pWhile program can be seen as the generator of a Discrete Time Markov Chain and plays a similar role as a collecting or trace semantics for classical While. Probabilistic Abstract Interpretation techniques are then employed in order to define data flow analyses for properties like Parity and Live Variables. |
| |
Keywords: | Probabilistic Programs Linear Operators Semantics Probabilistic Abstract Interpretation Data Flow Analysis |
本文献已被 ScienceDirect 等数据库收录! |