Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:


Written in Published in Earliest date Latest date

Sorted by

Results per page:

You searched for id:"handle:10919/89223". One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

Virginia Tech

1. Guo, Shengjian. 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

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Guo, S. (2019). Efficient Symbolic Execution of Concurrent Software. (Doctoral Dissertation). Virginia Tech. Retrieved from

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:

Council of Science Editors:

Guo S. Efficient Symbolic Execution of Concurrent Software. [Doctoral Dissertation]. Virginia Tech; 2019. Available from: