PV2 MU-CSeqsequentialises a parallel C program

Application domain/field

Type of tool

Concurrency preprocessor/code-to-code translator

Expected input


Expected output

Sequentialized version of the original program.


Sequentialization: Translate a concurrent program into a sequential one, using a code-to-code translation that preserves the property of interest. This sequential code is then analyzed using a symbolic sequential verification tool, e.g. CBMC.


Related papers

MU-CSeq 0.4: Individual Memory Location Unwindings (TACAS '16)

Last publication date

9 April 2016

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.