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)

• 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
• CompCert
• Gmeta
• libclang
• LCTD
• Pilsner
• CertiKOS
• Kami
• VST-Floyd
• Knuth Morris Pratt
• LCT
• IEEE_Floating_Point
• GraalVM
• Silq
• LCTD: test-guided proofs for C programs on LLVM
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Trace-relating compiler correctness and secure compilation
• A linear first-order functional intermediate language for verified compilers

This page was built for software: Vellvm