MU-CSeq: sequentialization of c programs by shared memory unwindings (competition contribution)
Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato · ePrints Soton (University of Southampton) · 2014
Abstract. We implement a new sequentialization algorithm for multi-threaded C programs with dynamic thread creation as a new CSeq module. The novel basic idea of this algorithm is to fix (by a nondeterministic guess) the sequence of write operations in the shared memory and then simulate the behavior of the program according to any scheduling that respects this choice. Simulation is done thread-by-thread and the thread creation mechanism is replaced by function calls. 1