Savel'ev

 The authors consider methods of synthesis and basic properties of various discrete basis systems of generalized Christenson functions in polybasic number systems, as well as the original scalar method of constructing fast algorithms for analyzing the spectrum in these bases. Theoretical results are illustrated with concrete examples.

Improving the verification of hardware and software systems is associated with the usage of formal methods among which the authors consider the model checking method which provides an automated consideration of all possible "paths of functioning" of the system. The problem of “explosion of the number of states” inherent in the method of verification of model checking is analyzed in the article; various methods of dealing with this problem are discussed. Particular attention is paid to verification of coherence memory protocols; possible approaches to solving this problem are outlined.