Formalizing the LLVM intermediate representation for verified program transformations
DOI10.1145/2103656.2103709zbMATH Open1321.68207OpenAlexW4298447450MaRDI QIDQ2942893FDOQ2942893
Authors: Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic 
Publication date: 11 September 2015
Published in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.228.6616
Recommendations
- Formal verification of a C-like memory model and its uses for verifying program transformations
- A Framework for Formal Verification of Compiler Optimizations
- Verifying optimizations for concurrent programs
- Mechanized verification of computing dominators for formalizing compilers
- A formally verified compiler back-end
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cited In (16)
- Cogent: uniqueness types and certifying compilation
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- A modeling concept for formal verification of OS-based compositional software
- Mechanized verification of computing dominators for formalizing compilers
- Title not available (Why is that?)
- A formal semantics of the GraalVM intermediate representation
- Title not available (Why is that?)
- Vellvm
- LCTD: test-guided proofs for C programs on LLVM
- Verifying constant-time implementations by abstract interpretation
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Proving Termination of C Programs with Lists
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Trace-relating compiler correctness and secure compilation
- A linear first-order functional intermediate language for verified compilers
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
Uses Software
This page was built for publication: Formalizing the LLVM intermediate representation for verified program transformations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942893)
