BRICK: A Bounded Verifier for C code
BRICK is a bounded reachability checker for numerically intensive C code, with special emphasis on handling nonlinear operations. It supports user-specified safety specification checking as well as built-in assertion checking.
Different from the existing tools, BRICK supports the checking of codes with nonlinear operations. e.g. trigonometric functions, exponential functions by delta-decision SMT solver dReal. BRICK has scaled well on realistic programs in evaluation, e.g. the benchmarks in SV-Comp.
BRICK returns the check result and generates a Witness file which shows the detailed information, e.g. the counter-example which triggers the assert statement.
download brick.zip to the directory you want and run Unix command:
unzip brick.zip
Attention: brick.zip is stored with Git LFS due to the file size.
BRICK verifies with following command in the standard unix command-line style:
cd brick
&&
./bin/brick < filename > -b < bound > -p < precision > [-options].
Lei Bu, Zhunyi Xie, Lecheng Lyu, Yichao Li, Xiao Guo, Jianhua Zhao and Xuandong Li