Boolean Programs

About

Boolean programs result from applying predicate abstraction to general software. All var­i­ables are of type Boolean, and track truth values of predicates over (possibly unbounded) var­i­ables of the original program P. To enable sound verification of reachability properties, Boolean programs are constructed by over-approximating the behavior of P. This may add spurious paths, which can be eliminated by refining the abstraction, using additional pre­di­cates. Several tools exist that translate C code into a Boolean program, e.g., SLAM and SatAbs.

Contact Information

Gérard Basler: gerard.basler@inf.ethz.ch

Example of a Boolean program

A tutorial how to generate Boolean programs is here:

Boolean program example 1

Extension to Concurrent Boolean Programs

SatAbs extends the semantics for sequential Boolean programs with 5 instructions to support concurrency:

Note that atomic_begin and atomic_end must not form nested blocks. This document provides an updated syntax for concurrent Boolean programs. 

A Parser Skeleton

A skeleton of a parser for concurrent Boolean programs can be found here:

Parser (bison): bp_parser.yy
Lexer (flex): bp_scanner.ll

It is able to parse Boolean programs generated by SLAM and SatAbs.

Tools

Reachability checker for concurrent Boolean programs:

Benchmark Collection

Further Reading

Symbolic Counter Abstraction for Concurrent Software
A Complete Bounded Model Checking Algorithm for Pushdown Systems
SAT-based Summarization for Boolean Programs
Model Checking Concurrent Linux Device Drivers
Over-Approximating Boolean Programs with Unbounded Thread Creation
Symbolic model checking for asynchronous Boolean programs

External Links

Reachability checker for sequential Boolean programs

Support

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

Last Update: Apr 16, 2009 by Gérard Basler.