Automated testing of LLVM programs with complex input data structures
Proceedings of the Institute for System Programming of the RAS(2022)
摘要
Symbolic execution is a widely used approach for automatic regression test generation and bug and vulnerability finding. The main goal of this paper is to present a practical symbolic execution-based approach for LLVM programs with complex input data structures. The approach is based on the well-known idea of lazy initialization, which frees the user from providing constraints on input data structures manually. Thus, it provides us with a fully automatic symbolic execution of even complex program. Two lazy initialization improvements are proposed for segmented memory models: one based on timestamps and one based on type information. The approach is implemented in the KLEE symbolic virtual machine for the LLVM platform and tested on real C data structures — lists, binomial heaps, AVL trees, red-black trees, binary trees, and tries.
更多查看译文
关键词
llvm programs,automated testing,complex input data structures
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要