Probabilistically Accurate Program Transformations

18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings

Bibliographic Details
Main Authors: Misailovic, Sasa (Contributor), Roy, Daniel (Contributor), Rinard, Martin C. (Contributor)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: Springer Berlin / Heidelberg, 2012-10-11T19:41:16Z.
Subjects:
Online Access:Get fulltext
LEADER 02220 am a22003013u 4500
001 73897
042 |a dc 
100 1 0 |a Misailovic, Sasa  |e author 
100 1 0 |a Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory  |e contributor 
100 1 0 |a Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science  |e contributor 
100 1 0 |a Misailovic, Sasa  |e contributor 
100 1 0 |a Roy, Daniel  |e contributor 
100 1 0 |a Rinard, Martin C.  |e contributor 
700 1 0 |a Roy, Daniel  |e author 
700 1 0 |a Rinard, Martin C.  |e author 
245 0 0 |a Probabilistically Accurate Program Transformations 
260 |b Springer Berlin / Heidelberg,   |c 2012-10-11T19:41:16Z. 
856 |z Get fulltext  |u http://hdl.handle.net/1721.1/73897 
520 |a 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings 
520 |a 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. 
520 |a National Science Foundation (U.S.) (Grant CCF-0811397) 
520 |a National Science Foundation (U.S.) (Grant CCF-0905244) 
520 |a National Science Foundation (U.S.) (Grant CCF-1036241) 
520 |a National Science Foundation (U.S.) (Grant IIS-0835652) 
520 |a United States. Dept. of Energy (Grant DE-SC0005288) 
546 |a en_US 
655 7 |a Article 
773 |t Static Analysis