Name
Abstract | ||
|---|---|---|
A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. In general, certificates cannot be generated automatically. There is thus an interest in developing methods to reuse certificates generated for source code to provide strong guarantees of the compiled code correctness. Certificate translation is a method to transform certificates of program correctness along semantically justified program transformations. These methods have been developed in previous work, but they were strongly dependent on particular programming and verification settings. This article provides a more general development in the setting of abstract interpretation, showing the scalability of certificate translation. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/1985342.1985344 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
abstract model,code correctness,semantically justified program transformation,abstract interpretation,source code,mathematical object,particular programming,general development,mobile code,certificate translation,program correctness,security policy,static analysis,satisfiability,program optimization | Unreachable code,Static program analysis,Programming language,Source code,Computer science,Correctness,Theoretical computer science,Redundant code,Proof-carrying code,Program analysis,Certificate | Journal |
Volume | Issue | ISSN |
33 | 4 | 0164-0925 |
Citations | PageRank | References |
2 | 0.38 | 35 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| César Kunz | 2 | 167 | 10.81 |