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:
- The Parma Polyhedra Library
- The Z3 SMT-solver
- The mcmt model-checker (and the SMT-solver Yices, as part of mcmt).
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.
Publications:
Theoretical and practical details about Booster can be found on the following papers:
- Decision Procedures for Flat Array Properties, F. Alberti, S. Ghilardi, N. Sharygina, (TACAS), Grenoble, France, April 5-13, 2014
- Booster: an acceleration-based verification framework for array programs, F. Alberti, S. Ghilardi, N. Sharygina, (ATVA), Sydney, Australia, November 3-7, 2014
