Model Checking Boolean Programs

About Boom

Boom is a model checker for concurrent Boolean programs.

Features:

• Summarization of procedures (path-wise and universal summaries) (sequential mode only)
• Structural abstraction of procedures (sequential mode only)
• Fixpoint detection using QBF / k-Induction
• Partial order reduction (ample sets + persistent sets / cartesian partial order reduction)
• Symbolic counter abstraction using BDDs
• Extension to unbounded thread creation (Karp-Miller)
• Unbounded thread creation over-approximation (with BDDs)
• Generates counterexamples for SLAM and SatAbs
• Cutoff analysis using BDDs

For questions about Boom contact gerard.basler@inf.ethz.ch.

You should also read the license.