Name
Abstract | ||
|---|---|---|
In a Proof-Carrying Code scenario, certificate generation remains a challenging problem. Typically, it is implemented as a compiler module that targets low-level executable code. Hence, since automatic, the properties under verification are limited to very simple safety policies. Discharging verification conditions automatically for arbitrarily complex properties is unfeasible. Therefore, it requires the support of tool-based interactive verification, which commonly targets high-level structured code. To connect source code verification and compiled code certification we have proposed a technique to build, from a certificate of the source program, a certificate for the result of its compilation. In this tutorial, we illustrate the principles of this technique, certificate translation, in the context of a certified quicksort algorithm. For each transformation step that defines the compiler, we explain the corresponding transformation of the certificate. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-642-03829-7_2 | FOSAD |
Keywords | Field | DocType |
certificate generation,compiler module,tool-based interactive verification,discharging verification condition,corresponding transformation,high-level structured code,low-level executable code,certificate translation,source code verification,code certification,source code | Dead code elimination,Unreachable code,Programming language,Source code,Computer science,Code generation,Redundant code,Certification path validation algorithm,Dead code,Certificate | Conference |
Volume | ISSN | Citations |
5705 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| César Kunz | 2 | 167 | 10.81 |