We describe a new CSeq module that implements improved algorithms for the verification of multi-threaded C programs with dynamic thread creation. It is based on sequentializing the programs according to a guessed sequence of write operations in the shared memory (memory unwinding, MU). The original algorithm (implemented in MU-CSeq 0.1) stores the values of all shared variables for each write (read-explicit fine-grained MU), which requires multiple copies of the shared variables. Our new algorithms store only the writes (readimplicit MU) or only a subset of the writes (coarse-grained MU), which reduces the memory footprint of the unwinding and so allows larger unwinding bounds.
CITATION STYLE
Tomasco, E., Inverso, O., Fischer, B., La Torre, S., & Parlato, G. (2015). MU-CSeq 0.3 Sequentialization by read-implicit and coarse-grained memory unwindings (competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9035, pp. 436–438). Springer Verlag. https://doi.org/10.1007/978-3-662-46681-0_38
Mendeley helps you to discover research relevant for your work.