Boppo – Model Checking Boolean Programs
Boppo is a model checker for Boolean programs. Features:
- Partial Order Reduction
- Fixpoint detection using QBF
- Support for the
- The ETH technical report describing Boppo is available here.
- Symbolic model checking for asynchronous Boolean programs (SPIN)
- Verification of Boolean Programs with Unbounded Thread Creation (FMCAD, TCS)