Automated Verification of Asynchronous Communicating Systems
Please refer to the
to learn how to use this website.
Numerous examples are also available
Add CCS peer
Add LTS peer
All peers terminate.
The network ends up empty.
No peer goes into a forbidden state.
No (global) deadlocks
Infer all constraint sets (pessimistic)
Infer one constraint set (pessimistic)
Infer some constraint sets (optimistic)
Infer one constraint set (optimistic)
Infer all constraint sets (pessimistic, listened)
Infer one constraint set (pessimistic, listened)
Infer some constraint sets (optimistic, listened)
Infer one constraint set (optimistic, listened)
Using CCS peers with the current pretty printer makes it difficult to identify the peers (as their order may change).
CCS peers are not supported.
Constraint inference easily times out, because the analyzers don't flush their output buffers often enough (at all?).