A verifiable SSA program representation for aggressive compiler optimization

DOI10.1145/1111037.1111072zbMATH Open1369.68080OpenAlexW2135488322WikidataQ130883839 ScholiaQ130883839MaRDI QIDQ5348941FDOQ5348941

Authors: Vijay Menon, Neal Glew, Brian R. Murphy, Andrew Mccreight, Tatiana Shpeisman, Ali-Reza Adl-Tabatabai, Leaf Petersen 

Publication date: 21 August 2017

Published in: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1111037.1111072

Recommendations

• A Framework for Formal Verification of Compiler Optimizations
• Compositional verification of compiler optimisations on relaxed memory
• scientific article; zbMATH DE number 1956470
• scientific article; zbMATH DE number 512903
• Verification, Model Checking, and Abstract Interpretation

zbMATH Keywords

type systemsintermediate representationscheck eliminationproof variablessafety dependencesSSA formalizationtypeability preservationtyped intermediate languages

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Cited In (4)

• Synthesizing JIT compilers for in-kernel DSLs
• Securing the SSA transform
• A formal semantics of the GraalVM intermediate representation
• Static single information form for abstract compilation

This page was built for publication: A verifiable SSA program representation for aggressive compiler optimization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5348941)