Practical Verification of Peephole Optimizations with Alive
We created Alive, a domain-specific language for writing correct peephole optimizations and for automatically either proving them correct or else generating counterexamples.
John Regehr
Advertisement
Author Archives
Research For Practice: Vigorous Public Debates in Academic Computer Science
Expert-curated guides to the best of CS research.
Technical Perspective: Stacking Up Undefined Behaviors
In "A Differential Approach to Undefined Behavior Detection," Wang et al. hypothesize that any time a compiler is able to delete code by using reasoning based on undefined behavior, the program being compiled probably contains a bug.
Shape the Future of Computing
ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.
Get Involved