Booster



Valid XHTML 1.0 Strict
Valid CSS!

menu  About 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:

Booster is built on the top of the following tools:

menu  Download

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

menu  Benchmarks

Booster has been evaluated on the following sets of benchmarks.

menu  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

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 );
       }
       
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