todo:

Notes related to LLVM compiler

Binary lifter, BinRec binary lifter, Capstone disassembler, Dagger binary lifter, KLEE verifier, LLVM-MCtoLL binary lifter, McSema binary lifter, Remill binary lifting library, reopt binary lifter, RetDec decompiler, rev.ng reverse engineering tool, S2E verifier, SeaHorn verifier, SecondWrite binary lifter, Serval solver-based verifier, SMACK verifier

Papers related to LLVM compiler

• BinRec: Dynamic binary lifting and recompilation [altinay:eurosys:2020]
• A compiler-level intermediate representation based binary analysis and rewriting system [anand:eurosys:2013]
• Verifying Rust programs with SMACK [baranowski:atva:2018]
• Rev.Ng: A unified binary analysis framework to recover CFGs and function boundaries [difederico:cc:2017]
• The SeaHorn verification framework [gurfinkel:cav:2015]
• LLVM: a compilation framework for lifelong program analysis and transformation [lattner:cgo:2004]
• LLBMC: Bounded model checking of C and C++ programs using a compiler IR [merz:vstte:2012]
• Dataflow-based pruning for speeding up superoptimization [mukherjee:oopsla:2020]
• Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
• Symbolic execution with SymCC: Don't interpret, compile! [poeplau:usenix:2020]
• SMACK: Decoupling source language details from verifier implementations [rakamaric:cav:2014]
• Raising binaries to LLVM IR with MCTOLL (WIP paper) [yadavalli:lctes:2019]