Vellvm

swMATH13286MaRDI QIDQ25201FDOQ25201

Author name not available (Why is that?)

Described by source

• Formalizing the LLVM intermediate representation for verified program transformations

Cited In (8)

• A Linear First-Order Functional Intermediate Language for Verified Compilers
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Trace-Relating Compiler Correctness and Secure Compilation
• A formal semantics of the GraalVM intermediate representation
• Title not available (Why is that?)
• LCTD: test-guided proofs for C programs on LLVM
• Proving Termination and Memory Safety for Programs with Pointer Arithmetic
• Mechanized Verification of Computing Dominators for Formalizing Compilers

This page was built for software: Vellvm