Formalizing the LLVM intermediate representation for verified program transformations
From MaRDI portal
Publication:2942893
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
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
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
