Assist
Several verification tools exist for checking safety properties of programs and reporting errors. However, a large part of the program development cycle is spend in analyzing the error trace to isolate locations in the code that are potential causes of the bug. We present Bug-Assist, a tool that assists programmers localize error causes to a few lines of code. Bug-Assist takes as input an ANSI-C program annotated with assertions, performs model checking internally to find potential assertion violations, and for each error trace returned by the model checker, returns a small number of lines of code which can be changed to eliminate the error trace. Bug-Assist's algorithm formulates error localization as a MAX-SAT problem and uses scalable MAX-SAT solvers. In experiments on a set of C benchmarks, Bug-Assist was able to reduce error traces to only a few lines of code. We have built an Eclipse plugin for Bug-Assist, enabling its easy deployment in the code development phase.
This is the first release of `Bug-Assist'. It is still considered pre-alpha software (Friends and family release). A lot of features are missing. If you want support on any other architectures or enhancements or source code, please contact us through mail. The best way to use the tool is with the eclipse plugin as described in the user manual. The eclipse plugin is heavily inspired by the existing CBMC eclipse plugin.
The command line executable are available for linux 32/64 bit versions. The tool can be used as follows "bugassist file.c --ba --maxsat < max-sat solver location >". The max sat solver option helps to try out new solvers as tool generates the SAT instance similar to the max-sat competition format. In our experiments we have used the msuncore tool. More options of fine tunning the model checker can be obtained with "--help" option.
