Name
Abstract | ||
|---|---|---|
Relational program logics are formalisms for specifying and verifying properties about two programs or two runs of the same program. These properties range from correctness of compiler optimizations or equivalence between two implementations of an abstract data type, to properties like non-interference or determinism. Yet the current technology for relational verification remains underdeveloped. We provide a general notion of product program that supports a direct reduction of relational verification to standard verification. We illustrate the benefits of our method with selected examples, including non-interference, standard loop optimizations, and a state-of-the-art optimization for incremental computation. All examples have been verified using the Why tool. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-21437-0_17 | FM |
Keywords | Field | DocType |
direct reduction,compiler optimizations,relational program logic,product program,relational verification,abstract data type,standard verification,standard loop optimizations,general notion,current technology | Abstract data type,Functional verification,Programming language,Computer science,Correctness,Theoretical computer science,Implementation,Optimizing compiler,Equivalence (measure theory),Rotation formalisms in three dimensions,Computation | Conference |
Citations | PageRank | References |
65 | 1.57 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| Juan Manuel Crespo | 2 | 164 | 7.25 |
| César Kunz | 3 | 167 | 10.81 |