Abstract
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 language | English (US) |
|---|---|
| Title of host publication | Static Analysis - 18th International Symposium, SAS 2011, Proceedings |
| Pages | 316-333 |
| Number of pages | 18 |
| DOIs | |
| State | Published - Sep 28 2011 |
| Externally published | Yes |
| Event | 18th International Static Analysis Symposium, SAS 2011 - Venice, Italy Duration: Sep 14 2010 → Sep 16 2010 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 6887 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 18th International Static Analysis Symposium, SAS 2011 |
|---|---|
| Country | Italy |
| City | Venice |
| Period | 9/14/10 → 9/16/10 |
Fingerprint
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Cite this
Probabilistically accurate program transformations. / Misailovic, Sasa; Roy, Daniel M.; Rinard, Martin C.
Static Analysis - 18th International Symposium, SAS 2011, Proceedings. 2011. p. 316-333 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6887 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Probabilistically accurate program transformations
AU - Misailovic, Sasa
AU - Roy, Daniel M.
AU - Rinard, Martin C.
PY - 2011/9/28
Y1 - 2011/9/28
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=80053107668&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80053107668&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-23702-7_24
DO - 10.1007/978-3-642-23702-7_24
M3 - Conference contribution
AN - SCOPUS:80053107668
SN - 9783642237010
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 316
EP - 333
BT - Static Analysis - 18th International Symposium, SAS 2011, Proceedings
ER -