PV1 ⊧ POET: Partial Order Exploration Toolanalyses a multi-threaded program to see if it conforms to expectations of the tool

Explicit-state model checker

Application domain/field

• Partial order reduction
• Net unfoldings
• Model checking
• State space exploration

Type of tool

Model checker

Expected input

Multi-threaded C program

Format:

(Restricted fragment of the) C

• Can use __poet_fail() to indicate an assert false
• Supports POSIX threads

Expected output

It can:

• "print the result of the front-end" (???)
• execute the system with a non-deterministic schedule
• perform explicit-state model checking