Formalizing the LLVM intermediate representation for verified program transformations

DOI10.1145/2103656.2103709zbMath1321.68207OpenAlexW4298447450MaRDI QIDQ2942893

Santosh Nagarakatte, Steve Zdancewic, Jianzhou Zhao, Milo M. K. Martin

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)

Related Items (12)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Trace-Relating Compiler Correctness and Secure Compilation ⋮ The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ A formal semantics of the GraalVM intermediate representation ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ Verifying constant-time implementations by abstract interpretation ⋮ A Linear First-Order Functional Intermediate Language for Verified Compilers ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mechanized Verification of Computing Dominators for Formalizing Compilers ⋮ Vellvm ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

• Coq

This page was built for publication: Formalizing the LLVM intermediate representation for verified program transformations