Environment model

Environment models emulate interactions of target programs or program fragments like Linux kernel loadable modules with their environment like libraries, user inputs, interruptions and so on. Ideally they should cover only those interaction scenarios that are possible during real executions, but usually this is not the case, so false alarms and missing bugs take place. Klever generates each environment model on the basis of specifications and it is represented as a number of additional C source files (models) bound with original ones through instrumentation.

Program fragment

Software verification tools can not check nontrivial requirements for large programs in a reasonable time. So Klever decomposes target programs into moderate-sized program fragments and generates independent verification tasks for all of them. Each program fragment represents a subset of program source files and information how to build them. Program fragments can intersect with each other. Linux kernel loadable modules can serve as a good example of program fragments.


A path to a root directory of a Klever source tree.


A path to a directory where Klever should be deployed. Although this directory can be one of standard ones like /usr/local/bin or /bin, it is recommended to use some specific one.


A path to a file with SSH RSA private key. It is not recommended to use your sensitive keys. Instead either create and use a specific one or use keys that are accepted in your groups to enable an access to other group members.


Username used to login to OpenStack.


A number of OpenStack instances to be deployed.