PV2 ⊧ MU-CSeqsequentialises a parallel C program

Application domain/field

• Multi-threaded programs
• Sequentialization
• Memory unwinding

Type of tool

Concurrency preprocessor/code-to-code translator

Expected input

• Multi-threaded program
• Specification file

Format:

• Multi-threaded program: C program
• Specification file: ?

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.