PV4 ⊧ SYCOprovides traces of deadlocks in a concurrent system

Systematic testing tool for message-passing concurrent programs

Application domain/field

• Partial-order reduction (POR)
• Concurrent programs
• Actor programs
• Message-passing programs

Type of tool

Testing tool

Expected input

ABS program

Format:

.abs file

Internals

• Actor programs: Programs consisting of computing entities called actors. Each actor has its own local state and thread of control. The actors communicate by exchanging messages asynchronously.
• Partial Order Reduction (POR): Algorithms that are based on the idea that some program interleavings can be considered equivalent, and that you only need to explore one interleaving per equivalence class.
• Uses VeryMax