Cited in
(21)- 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
- CompCert
- Gmeta
- libclang
- LCTD
- Pilsner
- CertiKOS
- Kami
- VST-Floyd
- Knuth Morris Pratt
- LCT
- IEEE_Floating_Point
- GraalVM
- Silq
- Mechanized verification of computing dominators for formalizing compilers
- LCTD: test-guided proofs for C programs on LLVM
- Trace-relating compiler correctness and secure compilation
- Proving termination and memory safety for programs with pointer arithmetic
- A formal semantics of the GraalVM intermediate representation
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
This page was built for software: Vellvm
