Probabilistically accurate program transformations

Sasa Misailovic, Daniel M. Roy, Martin C. Rinard

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the application of transformations that may change, within probabilistic accuracy bounds, the result that the program produces. Our new approach produces probabilistic guarantees of the form ℙ(|D|≥ B) ≤ε, ε ∈ (0, 1), where D is the difference between the results that the transformed and original programs produce, B is an acceptability bound on the absolute value of D, and ε is the maximum acceptable probability of observing large |D|. We show how to use our approach to justify the application of loop perforation (which transforms loops to execute fewer iterations) to a set of computational patterns.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 18th International Symposium, SAS 2011, Proceedings
Number of pages18
StatePublished - Sep 28 2011
Externally publishedYes
Event18th International Static Analysis Symposium, SAS 2011 - Venice, Italy
Duration: Sep 14 2010Sep 16 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6887 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Static Analysis Symposium, SAS 2011

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Probabilistically accurate program transformations'. Together they form a unique fingerprint.

Cite this