Eric Mullen, Zachary Tatlock, and Dan Grossman. Peek: A formally verified peephole optimization framework for x86. In 1st International Workshop on Coq for Programming Languages, CoqPL '15. ACM, 2015.

Peek is a first step toward adding support for assembly-level program analyses, transformations, and optimizations in CompCert. Currently, Peek focuses on x86 peephole transformations implemented and verified in Coq. Peek is designed to provide a modular interface requiring that each peephole optimization satisfy only local correctness properties. Our primary result establishes that, assuming the C calling convention, any peephole optimization satisfying these local properties preserves global program meaning.

bib | project | paper ] Back

This file was generated by bibtex2html 1.98.