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)

• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Proving termination and memory safety for programs with pointer arithmetic
• Mechanized verification of computing dominators for formalizing compilers
• A formal semantics of the GraalVM intermediate representation
• Title not available (Why is that?)
• LCTD: test-guided proofs for C programs on LLVM
• Trace-relating compiler correctness and secure compilation
• A linear first-order functional intermediate language for verified compilers

This page was built for software: Vellvm