|
About the BOOP Toolkit
|
The BOOP Toolkit was implemented within the scope
of the master's thesis
of
Georg Weißenbacher at the
Institute for Software
Technology at Graz
University of Technology.
It is based on the
SLAM project of Microsoft Research. The BOOP Toolkit
uses abstraction and refinement to determine the reachability
of program points in a C program. When the BOOP Toolkit is
applied on a C program, it repeatedly passes through three phases:
- Abstraction: We apply theorem proving and predicate
transformers to remove detail from a C program.
- Model Checking: A model checker is applied on the
abstract program to search for erroneous execution traces (with
respect to a specification that must be provided by the user).
- Refinement: If the model checker found an error
path which is feasible in the original C program, it is reported
to the user. If the path is infeasable, the abstraction is
refined by adding more detail and the process is reiterated.
|
|
|
News
|
|
Georg is now an associate professor in the
FORSYTE group of
TU Wien. He
was previously a postdoctoral research
associate at
Princeton University,
after graduating with a doctoral degree from
Oxford University.
|
|
We have implemented a nice heuristic to
handle programs with deep loops in
SATABS.
Check out our loop detection benchmarks and our CAV'06 paper
"Counterexamples with Loops for Predicate Abstraction".
|
|
|
The installation instructions were updated
after Flora Amato and
Andreas Polzer reported some problems with HOL98.
Please note that BOOP isn't actively maintainted
anymore. If you want to use an abstraction/refinement
framework for your research, I would recommend to use
my new tool
Wolverine.
The SLAM-based
Static Driver Verifier is distributed as part of the
Windows Driver Foundation and is now an industry-strength
verification tool.
|
|
|
Project members
|
|
The BOOP Toolkit was implemented by Georg Weißenbacher
as partly fulfillment of his master's thesis. The thesis
was written at the Institute for
Software Technology at Graz University of Technology. It
was supervised by Roderick Bloem.
|
| Georg Weißenbacher |
weissenb forsyte.at
|
| Roderick Bloem |
rbloemiaik.tugraz.at
|
|
|
Related work
|
|
The SLAM project
|
The SLAM project is conducted by Tom Ball and Sriram
K. Rajamani at Microsoft Research. The BOOP Toolkit
is basically a reimplementation of the C2BP and
Newton tool that are part of the SLAM Toolkit.
|
|
The BLAST Toolkit
|
The BLAST Toolkit pursues a similar abstraction/refinement
approach to check that software
satisfies behavioral properties of the interfaces it uses. It uses
lazy abstraction, i.e. it does not recalculate the complete abstract
program in each iteration step.
|
|
SATABS
|
SATABS is an abstraction verification framework that is based on
SAT solving. It was developed by Daniel Kröning at CMU and
is actively improved by him and his group at
ETH Zurich.
|
|
Java Pathfinder
|
Java Pathfinder is a tool that was developed by the Automated Software
Engineering group at NASA Ames. It is a verification and testing
environment for Java which integrates model checking,
program analysis and testing.
|
|
MOPED
|
The MOPED model checker is a model checker for Boolean programs
and pushdown automata. It is integrated into the BOOP Toolkit
and can be used together with the SLAM Toolkit.
|
|
|
Created by Georg Weißenbacher
|
|
