Boppo – Model Checking Boolean Programs

About Boppo

By Byron Cook, Daniel Kroening, and Natasha Sharygina.

Boppo is a model checker for Boolean programs. Features:

• Partial Order Reduction
• Fixpoint detection using QBF
• Support for the constrain construct

Documentation

• 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)

Download

• Linux x86 binary: boppo-1.2.tgz
• Windows x86 binary: boppo-1.1-win.zip
• Benchmarks
• You will also need Quantor.