Abstract
We present the MU-CSeq tool for the verification of multithreaded 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.
Cite
CITATION STYLE
Tomasco, E., Nguyen, T. L., Inverso, O., Fischer, B., La Torre, S., & Parlato, G. (2016). MU-CSeq 0.4: Individual memory location unwindings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 938–941). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_65
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
