Paper Info
Title
Programs from proofs of predicated dataflow analyses
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 dataflow analyses. More precisely, we show how an imprecise but fast dataflow 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 dataflow analysis alone can yield precise results. An experimental evaluation practically supports our claim of easy verification.
Year
DOI
Venue
2015
10.1145/2695664.2695690
SAC 2015: Symposium on Applied Computing Salamanca Spain April, 2015
Keywords
Field
DocType
Programs from Proofs, Proof Carrying Code, Verification, Program transformation
Programming language,Program transformation,Correctness proofs,Computer science,Theoretical computer science,Verifiable secret sharing,Dataflow,Proof-carrying code,Mathematical proof,Predicate analysis
Conference
ISBN
Citations 
PageRank 
978-1-4503-3196-8
4
0.39
References 
Authors
18
2
Name
Order
Citations
PageRank
Marie-Christine Jakobs1325.51
Heike Wehrheim21013104.85