Boolean programs result from applying predicate abstraction to general software. All variables are of type Boolean, and track truth values of predicates over (possibly unbounded) variables 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 predicates. Several tools exist that translate C code into a Boolean program, e.g., SLAM and SatAbs.
Gérard Basler: email@example.com
A tutorial how to generate Boolean programs is here:Boolean program example 1
SatAbs extends the semantics for sequential Boolean programs with 5 instructions to support concurrency:
- The start_thread label instruction creates a new thread that starts execution at the program location label. It gets a copy of the local variables of the current thread, which continues execution at the proceeding statement.
- The end_thread statement terminates the actual thread, i.e., has no successor state.
- The atomic_begin statement prevents the scheduler from a context switch to an other thread.
- The atomic_end instruction allows any thread to be executed.
- sync instruction: not used.
Note that atomic_begin and atomic_end must not form nested blocks. This document provides an updated syntax for concurrent Boolean programs.
A skeleton of a parser for concurrent Boolean programs can be found here:
Reachability checker for concurrent Boolean programs:
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
Reachability checker for sequential Boolean programs
This research is currently supported by a grant from the Swiss National Science Foundation.
Last Update: Apr 16, 2009 by Gérard Basler.