Vellvm

MaRDI QIDQ25201swMATHFDO

Official website http://www.cis.upenn.edu/~stevez/vellvm/

Described by source

• Formalizing the LLVM intermediate representation for verified program transformations

Cited in

(21)

• A formal semantics of the GraalVM intermediate representation
• CompCert
• Gmeta
• libclang
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• A linear first-order functional intermediate language for verified compilers
• LCTD
• Pilsner
• Proving termination and memory safety for programs with pointer arithmetic
• CertiKOS
• LCTD: test-guided proofs for C programs on LLVM
• VST-Floyd
• Kami
• Knuth Morris Pratt
• LCT
• IEEE_Floating_Point
• Mechanized verification of computing dominators for formalizing compilers
• Trace-relating compiler correctness and secure compilation
• GraalVM
• Silq
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)

This page was built for software: Vellvm