Formation of the reverse example at verification of the algorithms using the methods of logical inference

This paper proposes a modification of the inference method by clause division based on the defining element. The method is one of the basic components of the software complex for parallel algorithms formal verification using the technique of model checking and mathematical appa-ratus of the theory of inference. The considered modification can not only detect the presence or absence of an error in the object of the analysis, but also, in case of error detection, restore the course of events leading to the occurrence of abnormal situation. The obtained information facilitates the process of error localization and contributes to its effective elimination. The study also introduces the concept of inference process scheme in relation to the problem of formal verification and proposes a set of graphic primitives for its description.