Abstract: Symbolic execution is a useful method in program verifying. But most symbolic execution tools don’t support multi-thread program. This paper analyzes the existed tools which support multi-thread program, and finds these problems: 1) some tools have good performance, but do not support lib, and hard to use practically; 2) some tools support lib, but are too old to upgrade, and can not find some basic bugs such as subtraction overflow, multiplication overflow and shift overflow. To solve these problems, this paper designs and implements MTSE(Multi-Thread Symbolic Execution) based on KLEE. MTSE supports multi-thread program with libc and libc++. MTSE can find 50% more bugs than Cloud9, and bring about 30% improvement in both instruction coverage and branch coverage compared with Cloud9.

Key words: symbolic execution, multi-thread program, program analysis