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:

 C:  

 cd C:Program FilesMicrosoft Visual StudioVC98Bin  

 call VCVARS32.BAT  

 F:  

 cd F:bat  

 cl test-comb.c  

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