PV3 ⊧ POR-SEchecks properties of multi-threaded programs by symbolic execution

Tool for systematic testing of multithreaded programs. It can handle programs with input (data) and concurrency.

Application domain/field

• Symbolic execution
• Partial-order reduction
• Multithreaded programs
• Concurrency
• Systematic testing

Type of tool

Testing tool?

Expected input

Format:

C program?

Internals

• POR-SE combines quasi-optimal partial order reduction (POR) with symbolic execution (SE).
• It has been implemented as an extension of KLEE (it is basically a multi-threaded extension of it).