PV2 MU-CSeqsequentialises a parallel C program

Application domain/field

Type of tool

Concurrency preprocessor/code-to-code translator

Expected input

Format:

Expected output

Sequentialized version of the original program.

Internals

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.
C

Links

Related papers

https://doi.org/10.1007/978-3-662-49674-9_65 (TACAS '16)

Last publication date

9 April 2016

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.