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.