B2

A software model checker based on counterexample-based abstraction refinement
B2 is a re-implementation of the Blast software model checker for C programs. The re-implementation emphasizes cleaner design and exendible APIs over speed, making it a better test-bed for software verification.

B2 implements a lazy abstraction algorithm, with interpolation-based refinement, as in Blast. We hope that the simple design will make extending the basic algorithms easier.

Please send requests / comments / questions to Ranjit Jhala

or Rupak Majumdar.




License


Copyright 2006-2008 Regents of California

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.



Getting Started


Linux binaries are b2-linux.tgz. Binaries plus source code is b2.tgz. Note that you need the Simplify theorem prover executable in your path when you run B2.

This is a pre-alpha "friends and family" release and has bugs (we know!). So we won't even give a "version number" for the release.

Imprint / Data Protection