Configure Booster

Booster can be configured by modifying the options in the config file. To generate the default template of the config file, simply execute 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.