Authors
Ermenegildo Tomasco, Truc L Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
Publication date
2016
Conference
Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings 22
Pages
938-941
Publisher
Springer Berlin Heidelberg
Description
We present the MU-CSeq tool for the verification of multi-threaded C programs with dynamic thread creation, dynamic memory allocation, and pointer arithmetic. It is based on sequentializing the programs over the new notion of individual memory location unwinding (IMU). IMU is derived from the notion of memory unwinding that has been implemented in the previous versions of MU-CSeq. The main concepts of IMU are: (1) the use of multiple write sequences, one for each individual shared memory location that is effectively used in the executions and (2) the use of memory addresses rather than variable names in the operations on the shared memory, which requires a separate table to map write sequences but supports pointer arithmetic.
Scholar articles
E Tomasco, TL Nguyen, O Inverso, B Fischer… - Tools and Algorithms for the Construction and Analysis …, 2016