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