Program Analysis Probably Counts

Abstract. Semantics-based program analysis uses an abstract semantics of programs/systems to statically determine run-time properties. Classic examples from compiler technology include analyses to support constant propagation and constant folding transformations and estimation of pointer values to prevent buffer overruns. More recent examples include the estimation of information flows (to enforce security constraints) and estimation of non-functional properties such as timing (to determine worst case execution times in hard real-time applications). The classical approaches are based on semantics involving discrete mathematics. Paralleling trends in model-checking, there have been recent moves towards using probabilistic and quantitative methods in program analysis. In this paper we will start by reviewing both classical and probabilistic/quantitative approaches to program analysis. We will provide a comparison of the two approaches. We will use a simple information flow analysis to ex...

• Type: Journal
• Year: 2010
• Where: CJ
• Authors: Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky
• Keywords: CJ 2010, Constant Folding Transformations, Image Analysis, Program Analysis, Semantics-based Program Analysis