目前看過的幾篇論文都是講在LLVM IR上面做程式分析相關的工作的，下面就它們各自的特點進行總結：

LLMBC主要用於邊界模型檢測，支援C和C++語言，通過將LLVM intermediaterepresentation轉換成為邏輯表示式，使用重寫規則化簡，轉換成為自定義的中間語言ILR，然後將ILR作為SMT求解器的輸入進行求解。目前支援的算術上溢和下溢，邏輯和算術移位超過位寬，無效地址的記憶體訪問，無效的記憶體申請，無效的記憶體釋放，memcpy的記憶體區域重疊，記憶體洩露，使用者自定義的斷言，BMC特定的斷言。缺點：還不能支援C++的浮點數、異常處理和執行時型別資訊。且不開源，不能追蹤缺陷到原始碼層（

LAV是一個用來靜態檢測程式斷言和程式錯誤的開源工具。它在基本塊內部採用符號執行生成一階邏輯表示式，基本塊之間採用謂詞邏輯，這樣就產生了無迴圈的多項式驗證的條件。其對於迴圈的處理採用了兩種方法：underapproximate和overapproximate兩種展開技術。然後將其中的多項式驗證調價放入SMT求解器。可解決問題：緩衝區溢位，除零和根據斷言檢測程式的正確性。可以支援fortran中的一些小問題，缺點還需要對面向物件語言進行支援（futurework），還不支援遞迴程式和浮點運算。

KLOVER是一個針對C++的符號執行和自動用例生成的工具，主要講了一些從C