HybVeri is an efficient software model checker for safety property verification of C programs.
Download and Installation:
The tool is avaible at Here (part-1,part-2, part-3, part-4, part-5). The platform is Windows OS and Eclipse. First, you need to install a Java Runtime Envirnment which is at least Java 7 comptble. Second, you need to create a folder F:at and put the following file inside:
exeProgram.bat: the file can compile test-comb.c to generate the test-comb.exe. test-comb.c is a temporal file to run the complex loops. The content of exeProgram.bat is as follows:
cd C:Program FilesMicrosoft Visual StudioVC98Bin
The directory C:Program FilesMicrosoft Visual StudioVC98Bin is the location of the file VCVARS32.BAT. You need to replace it with your directory.
How to use?
1. Choose a source code file (C program) that you want to check.
2. Choose a configuration file. Standard configuration files can be found in the directory config. Choose the file predicateAnalysis-PredAbsRefiner-SBE.properties .
3. Execute the command "java -jar HybVeri.jar [ -config <CONFIG_FILE> ] < SOURCE_FILE>", e.g. java –jar HybVeri.jar -config configpredicateAnalysis-PredAbsRefiner-SBE.properties example.c.
Experiments: Crude Data