Савельев Александр Яковлевич

Рассмотрены методы синтеза и основные свойства различных дискретных базисных систем обобщенных функций Крестенсона в многоосновных системах счисления, а так же оригинальный скалярный способ построения быстрых алгоритмов анализа спектра в этих базисах. Теоретические результаты проиллюстрированы конкретными примерами.

 Улучшение результатов верификации аппаратных и программных систем связывается с применением формальных методов, среди которых авторы выделяют метод model checking, обеспечивающий автоматизированное рассмотрение всех возможных «траекторий функционирования» системы. Анализируется проблема «взрыва числа состояний», свойственная верификации методом model checking, и рассматриваются различные методы борьбы с этой проблемой. Особое внимание уделяется верификации протоколов когерентности памяти и излагаются возможные подходы к решению данной задачи.