Vellvm

swMATH13286MaRDI QIDQ25201FDOQ25201

Author name not available (Why is that?)

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

This page was built for software: Vellvm