Programs from Proofs of Predicated Dataflow Analyses

M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015, pp. 1729–1736.

Download
Restricted 262-mainSACfinal.pdf 554.58 KB
Conference Paper
Author
;
Abstract
Programs from Proofs" is a generic method which generates new programs out of correctness proofs of given programs. The technique ensures that the new and given program are behaviorally equivalent and that the new program is easily verifiable, thus serving as an alternative to proof-carrying code concepts. So far, this generic method has one instantiation that verifies type-state properties of programs. In this paper, we present a whole range of new instantiations, all based on data ow analyses. More precisely, we show how an imprecise but fast data ow analysis can be enhanced with a predicate analysis as to yield a precise but expensive analysis. Out of the safety proofs of this analysis, we generate new programs, again behaviorally equivalent to the given ones, which are easily verifiable" in the sense that now the data ow analysis alone can yield precise results. An experimental evaluation practically supports our claim of easy verification.
Publishing Year
Proceedings Title
Proceedings of the 30th Annual ACM Symposium on Applied Computing
Page
1729-1736
LibreCat-ID

Cite this

Jakobs M-C, Wehrheim H. Programs from Proofs of Predicated Dataflow Analyses. In: Proceedings of the 30th Annual ACM Symposium on Applied Computing. SAC ’15. ; 2015:1729-1736. doi:10.1145/2695664.2695690
Jakobs, M.-C., & Wehrheim, H. (2015). Programs from Proofs of Predicated Dataflow Analyses. In Proceedings of the 30th Annual ACM Symposium on Applied Computing (pp. 1729–1736). https://doi.org/10.1145/2695664.2695690
@inproceedings{Jakobs_Wehrheim_2015, series={SAC ’15}, title={Programs from Proofs of Predicated Dataflow Analyses}, DOI={10.1145/2695664.2695690}, booktitle={Proceedings of the 30th Annual ACM Symposium on Applied Computing}, author={Jakobs, Marie-Christine and Wehrheim, Heike}, year={2015}, pages={1729–1736}, collection={SAC ’15} }
Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs of Predicated Dataflow Analyses.” In Proceedings of the 30th Annual ACM Symposium on Applied Computing, 1729–36. SAC ’15, 2015. https://doi.org/10.1145/2695664.2695690.
M.-C. Jakobs and H. Wehrheim, “Programs from Proofs of Predicated Dataflow Analyses,” in Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015, pp. 1729–1736.
Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs of Predicated Dataflow Analyses.” Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015, pp. 1729–36, doi:10.1145/2695664.2695690.
Main File(s)
File Name
262-mainSACfinal.pdf 554.58 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-03-21T09:35:34Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar