Testing Programs with Contextual Unfoldings

Research output: Contribution to journalArticleScientificpeer-review


Original languageEnglish
Article number23
Pages (from-to)1-25
JournalACM Transactions on Embedded Computing Systems
Issue number1
Publication statusPublished - 1 Nov 2017
MoE publication typeA1 Journal article-refereed


Research units


In this article, we present a new algorithm that combines contextual unfoldings and dynamic symbolic execution to systematically test multithreaded programs. The approach uses symbolic execution to limit the number of input values and unfoldings to thus limit the number of thread interleavings that are needed to cover reachable local states of threads in the program under test. We show that the use of contextual unfoldings allows interleavings of threads to be succinctly represented. This can in some cases lead to a substantial reduction in the number of needed test executions when compared to previous approaches.

    Research areas

  • testing, contextual unfoldings, dynamic symbolic execution

ID: 16820057