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.

Boom Publications

• SAT-based Summarisation for Boolean Programs
• A Complete Bounded Model Checking Algorithm for Pushdown Systems
• New: Symbolic Counter Abstraction for Concurrent Software

Download

We currently distribute binaries for Linux and Windows. Please note that you will need to install sKizzo.

Date Windows Linux 7-Feb-2013 on request boom-1.8-linux-x86.tar.bz2 22-Mar-2010 on request boom-1.7-linux-x64.tar.bz2 boom-1.7-linux-x86.tar.bz2 11-Oct-2009 boom-1.6-windows-x86.zip boom-1.6-linux-x64.tar.bz2 boom-1.6-linux-x86.tar.bz2 28-Mar-2009 on request boom-1.5-linux-x64.tar.bz2 boom-1.5-linux-x86.tar.bz2 2-Feb-2009 on request boom-1.4-linux-x64.tar.bz2 31-Dec-2008 on request boom-1.3-linux-x64.tar.bz2 23-Okt-2008 on request boom-1.2-linux-x64.tar.bz2 boom-1.2-linux-x86.tar.bz2 17-Jan-2008 --- boom-1.1.tar.gz 07-Jan-2008 --- boom-1.0.tar.gz

This research is supported by a grant from the Swiss National Science Foundation and by EPSRC.