Skip Navigation



The Computer Journal Advance Access published online on April 27, 2009
The Computer Journal, doi:10.1093/comjnl/bxp033
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Di Pierro, A.
Right arrow Articles by Wiklicky, H.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author 2009. Published by Oxford University Press on behalf of The British Computer Society. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Program Analysis Probably Counts

Alessandra Di Pierro1, Chris Hankin2,* and Herbert Wiklicky2

1 Department of Computer Science, University of Verona, Ca’ Vignal 2 - Strada le Grazie 15, I-37134 Verona, Italy
2 Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2AZ, UK

* Corresponding author: clh{at}doc.ic.ac.uk

Received 9 March 2009; revised 9 March 2009

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 start by reviewing both classical and probabilistic/quantitative approaches to program analysis. We shall provide a comparison of the two approaches. We shall use a simple information flow analysis to exemplify the classical approach. The existence of covert information flows through timing channels are difficult to detect using classical techniques; we show how such problems can be addressed using probabilistic techniques.

Key Words: program analysis • semantics • abstract interpretation

Handling editor: Erol Gelenbe


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.