Booster is a software model-checker devised for verifying imperative programs with arrays. The verification process inside Booster is manily based on acceleration procedures. Theoretical and practical details about Booster can be found on the following papers:
-
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, April 5-13, 2014
-
12th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sydney, Australia, November 3-7, 2014
Booster is built on the top of the following tools:
- The Parma Polyhedra Library
- The Z3 SMT-solver
- The mcmt model-checker (and the SMT-solver Yices, as part of mcmt).
Download
We provide the following versions of Booster (for linux systems):
- 32 bit architecture, statically linked, size: 36.47 MB, md5sum: 9a719f92d2ad7d263bda7f912b5785b4
- 64 bit architecture, statically linked, size: 48.37 MB, md5sum: 4c2c5b1fc8f249dd746773f16df0106c
Benchmarks
Booster has been evaluated on the following sets of benchmarks.
- standard - Programs with arrays used in related works on array analysis.
- sorting - Sorting procedures for arrays.
- data_structures - Programs exploiting arrays for defining more complex data-structures (e.g., sets).
- sanfoundry - Programs taken and adapted from the webpage www.sanfoundry.com/c-programming-examples-arrays/.
Some Booster programs have been adopted by the SV-COMP organizers for a new track of the competition (see svn.sosy-lab.org/software/sv-benchmarks/trunk/c/array-examples/).
Results of the experimental evaluation of Booster are available for the safe and unsafe benchmarks.
Tutorial
Syntax and Semantics
Booster parses a C-like language. In its actual implementation, it supports multi-procedural programs without recursion. Arrays can be declared with symbolic lengths. Semantically, an array is interpreted as a function. Accessing an array in a non-initialized position simply return an unknown value. When array are passed as parameters, Booster assumes the pass-by-reference semantics. Procedures cannot return arrays.
Configure Booster
Booster can be configured by modifying the options in the config file. To generate the default template of the config file, simply exectute Booster:
booster --config=booster.conf example.c
where booster.conf is the name of the configuration file you want to generate.
The options of Booster are
verbose N
-- set the verbosity to N.time_passes
-- displays the running time for each task executed by the tool.z3_timeout N
-- set the timeout of Z3, the SMT-solver exploited by Booster, to N (in milliseconds).z3_seed N
-- set the random seed of Z3 to N.abstraction
-- when executed with the mcmt fixpoint engine, enables abstraction features of mcmt.acceleration
-- enables acceleration features (see our paper at FroCoS 2013).acceleration_dp
-- enables the decision procedure based on acceleration (see our paper at TACAS 2014).bmc_depth N
-- the number of unwindings performed by the BMC module.produce_dot_cfgs
-- produces graphviz-compliant files for the control-flow graphs of the input source.abstract_domain polyhedra
-- enables an abstract interpreter based on polyhedra.widening_iterations 2
-- number of iterations before applying widening.n_threads N
-- executes N parallel copies of the fixpoint engine, each with different settings.output_file F
-- generates the file F containing the intermediate representation for the fixpoint engine.
Running example
In this example we will write a simple program initializing all the cells of an array to a given value. We start from the procedure receiving as input the array to initialize, the size of the array and the value.
void init ( int array[ ] , int size , int value ) { int i = 0; while ( i < size ) { array[ i ] = value; i = i + 1; } }
Recall that Booster assumes the pass-by-reference paradigm when array variables are given as parameters.
We now want to call the function init
from the main
:
#define SIZE void main( void ) { // Declaration of arrays of unknown length is OK for Booster. int a[ SIZE ]; // Uninitialized variables have an unknown value. int v; // call the init procedure init( a , SIZE , v ); }
Programs are checked with respect to their assertions. Booster allows to specify standard C assertions and universally quantified assertions. For our example, we want to check that, after the execution of init
, the array has been initialized in all its positions from 0 to SIZE
. We can specify this property in two ways: (i) a for
loop checking every single position of the array or (ii) a quantified assertion. The for-loop is the standard loop we would write in a C program:
int x; for ( x = 0 ; x < SIZE ; x++ ) { assert( a[ x ] == v ); }
<span text-align:="" justify;"="">The quantified assertion, instead, offers a more convenient way (both from the user readability perspective and from the verification point of view) to express such property:
assert( forall (int x) :: ( 0 <= x && x < SIZE ) ==> ( a[ x ] == v ) );
The final program will look like this:
#define SIZE /* * Procedures have to be defined before they are actually called inside other procedures. */ void init ( int array[ ] , int size , int value ) { int i = 0; while ( i < size ) { array[ i ] = value; i = i + 1; } } void main( void ) { int a[ SIZE ]; int v; init( a , SIZE , v ); assert( forall (int x) :: ( 0 <= x && x < SIZE ) ==> ( a[ x ] == v ) ); }
The execution of Booster on this file (and the default template configuration file) prints the following output:
# This is booster v0.1 (Beta) # Linked to Z3 version 4.3.1.0 # Random seed for Z3 set to 0 The program is safe