Modular and local reasoning about object-oriented programs has been widely studied for programing languages such as C# and Java. Once source programs have been proven, the next verification challenge is to ensure that the code produced by the compiler is correct. Since verifying a compiler can be extremely complex, this paper uses proof-transforming compilation, an alternative approach which automatically generates certificates, a bytecode proof, from proofs in the source language. The paper develops a bytecode logic using separation logic, and proof translation from proofs of object-oriented programs to bytecode. The translation also handles proofs for concurrent programs. The bytecode logic and the proof transformation are proven sound. © Springer International Publishing Switzerland 2014.
CITATION STYLE
Nordio, M., Calcagno, C., & Meyer, B. (2014). Certificates and separation logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8358 LNCS, pp. 273–293). Springer Verlag. https://doi.org/10.1007/978-3-319-05119-2_16
Mendeley helps you to discover research relevant for your work.