Booster

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:

  • F. Alberti, S. Ghilardi, N. Sharygina, "Decision Procedures for Flat Array Properties"
    20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, April 5-13, 2014
  • F. Alberti, S. Ghilardi, N. Sharygina, "Booster: an acceleration-based verification framework for array programs"
    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:

Download

We provide the following versions of Booster (for linux systems):

Benchmarks

Booster has been evaluated on the following sets of benchmarks.

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