Klever

Currently, program decomposition is controlled by configuration parameters of four sections in job.json which is too complicated for beginners. We propose to implement a separate file with configuration parameters and templates for different kinds of programs and approaches to program decomposition. In job.json few options remain such as program type, target code for verification and a way for decomposition, e.g. verify kernel subsystems or modules. The new file will contain in addition to the description of decomposition strategies ready to use fragmentation sets prepared for some programs with described decomposition to start with. Such sets contain an explicit enumeration of fragments.