LLBMC: improved bounded model checking of c programs using LLVM
TACAS'13 Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems（2013）
摘要
LLBMC is a tool for detecting bugs and runtime errors in C and C++ programs. It is based on bounded model checking using an SMT solver and thus achieves bit-accurate precision. A distinguishing feature of LLBMC in contrast to other bounded model checking tools for C programs is that it operates on a compiler intermediate representation and not directly on the source code.
更多查看译文
关键词
distinguishing feature,compiler intermediate representation,improved bounded model checking,bit-accurate precision,bounded model checking tool,source code,c program,runtime error,smt solver,bounded model checking
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要