Booster is a software model-checker devised for verifying imperative programs with arrays. The verification process inside Booster is mainly based on acceleration procedures. Booster is built on top of the following tools:

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 returns an unknown value. When arrays are passed as parameters, Booster assumes the pass-by-reference semantics. Procedures cannot return arrays.



Theoretical and practical details about Booster can be found on the following papers:

  1. Decision Procedures for Flat Array Properties, F. Alberti, S. Ghilardi, N. Sharygina, (TACAS), Grenoble, France, April 5-13, 2014
  2. Booster: an acceleration-based verification framework for array programs, F. Alberti, S. Ghilardi, N. Sharygina, (ATVA), Sydney, Australia, November 3-7, 2014