Formal verification of translation validators: a case study on instruction scheduling optimizations

    Symposium on Principles of Programming Languages, pp. 17-27, 2008.

    Cited by: 84|Bibtex|Views10|Links
    EI
    Keywords:
    verified compilerscoq proofinstruction scheduling optimizationstranslation validationlist schedulingMore(7+)

    Abstract:

    Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of its se- mantics. This approach can be used in a verified compiler, pro- vided that validation is formally proved to be correct. We present two such validators and their Coq proofs of correctness. The val- idators a...More

    Code:

    Data:

    Your rating :
    0

     

    Tags
    Comments