Formalizing the LLVM intermediate representation for verified program transformations

DOI10.1145/2103656.2103709MaRDI QIDQ2942893zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

Coqmemory safetyLLVM

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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

Cited in

(16)

• Transforming concurrent programs with semaphores into logically constrained term rewrite systems
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Leveraging compiler intermediate representation for multi- and cross-language verification
• A modeling concept for formal verification of OS-based compositional software
• Proving Termination of C Programs with Lists
• Automatically proving termination and memory safety for programs with pointer arithmetic
• A linear first-order functional intermediate language for verified compilers
• Vellvm
• Cogent: uniqueness types and certifying compilation
• Mechanized verification of computing dominators for formalizing compilers
• Grounding game semantics in categorical algebra
• LCTD: test-guided proofs for C programs on LLVM
• Trace-relating compiler correctness and secure compilation
• A formal semantics of the GraalVM intermediate representation
• Verifying constant-time implementations by abstract interpretation
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

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)