Efficient Symbolic Execution of Concurrent Software.
Degree: PhD, Electrical and Computer Engineering, 2019, Virginia Tech
Concurrent software has been widely utilizing in computer systems owing to the highly efficient
computation. However, testing and verifying concurrent software remain challenging tasks. This
matter is not only because of the non-deterministic thread interferences which are hard to reason
about but also because of the large state space due to the simultaneous path and interleaving explosions. That is, the number of program paths in each thread may be exponential in the number of branch conditions, and also, the number of thread interleavings may be exponential in the number of concurrent operations. This dissertation presents a set of new methods, built upon symbolic execution, a program analysis technique that systematically explores program state space, for testing concurrent programs. By modeling both functional and non-functional properties of the programs as assertions, these new methods efficiently analyze the viable behaviors of the given concurrent programs. The first method is assertion guided symbolic execution, a state space reduction technique that identifies and eliminates redundant executions w.r.t the explored interleavings. The second method is incremental symbolic execution, which generates test inputs only for the influenced program behaviors by the small code changes between two program versions. The third method is SYMPLC, a technique with domain-specific reduction strategies for generating tests for the multitasking Programmable Logic Controller (PLC) programs written in languages specified by the IEC 61131-3 standard. The last method is adversarial symbolic execution, a technique for detecting concurrency related side-channel information leaks by analyzing the cache timing behaviors of a concurrent program in symbolic execution. This dissertation evaluates the proposed methods on a diverse set of both synthesized programs and real-world applications. The experimental results show that these techniques can significantly outperform state-of-the-art symbolic execution tools for concurrent software.
Advisors/Committee Members: Wang, Chao (committeechair), Hsiao, Michael S. (committeechair), Zeng, Haibo (committee member), Yang, Yaling (committee member), Meng, Na (committee member), Lee, Dongyoon (committee member).
Subjects/Keywords: Symbolic Execution; Concurrency; Predicate summary; Change impact analysis; Programmable logic controller; Side-channel leak
to Zotero / EndNote / Reference
APA (6th Edition):
Guo, S. (2019). Efficient Symbolic Execution of Concurrent Software. (Doctoral Dissertation). Virginia Tech. Retrieved from http://hdl.handle.net/10919/89223
Chicago Manual of Style (16th Edition):
Guo, Shengjian. “Efficient Symbolic Execution of Concurrent Software.” 2019. Doctoral Dissertation, Virginia Tech. Accessed May 25, 2019.
MLA Handbook (7th Edition):
Guo, Shengjian. “Efficient Symbolic Execution of Concurrent Software.” 2019. Web. 25 May 2019.
Guo S. Efficient Symbolic Execution of Concurrent Software. [Internet] [Doctoral dissertation]. Virginia Tech; 2019. [cited 2019 May 25].
Available from: http://hdl.handle.net/10919/89223.
Council of Science Editors:
Guo S. Efficient Symbolic Execution of Concurrent Software. [Doctoral Dissertation]. Virginia Tech; 2019. Available from: http://hdl.handle.net/10919/89223