7 papers:
TACAS-2013-FalkeMS #bound #c #contest #model checking #named #source code #using- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM — (Competition Contribution) (SF, FM, CS), pp. 623–626.
PLDI-2013-ZhaoNMZ #optimisation #verification- Formal verification of SSA-based optimizations for LLVM (JZ, SN, MMKM, SZ), pp. 175–186.
- TACAS-2012-SinzMF #bound #contest #model checking #named #representation
- LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation — (Competition Contribution) (CS, FM, SF), pp. 542–544.
POPL-2012-ZhaoNMZ #formal method #program transformation #representation- Formalizing the LLVM intermediate representation for verified program transformations (JZ, SN, MMKM, SZ), pp. 427–440.
- PLDI-2011-TristanGM #validation
- Evaluating value-graph translation validation for LLVM (JBT, PG, GM), pp. 295–305.
CAV-2011-SteppTL #validation- Equality-Based Translation Validator for LLVM (MS, RT, SL), pp. 737–742.
CGO-2004-LattnerA #compilation #framework #named #program analysis- LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation (CL, VSA), pp. 75–88.
