- Daniel Kroening
- SMT Lists/Sets/Maps
- Google groups:
Boolean Programs
About
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.
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 1Extension to Concurrent Boolean Programs
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 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:
- Concurrent Boolean programs (110 MB) generated by DDVerify
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.