Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.4'2
Номер:6 (82)
Скачать PDF0 Кбайт
ПРИМЕНЕНИЕ ЗАВИСИМЫХ СИСТЕМ ТИПОВ СО СТРУКТУРНОЙ ИНДУКЦИЕЙ ДЛЯ ВЕРИФИКАЦИИ РЕАКТИВНЫХ ПРОГРАММ
Аннотация:
Предлагается конструктивное доказательство (в виде программы на языке Agda) того, что решение задачи о выполнимости булевой формулы при помощи исчисления секвенций и верификация с использованием темпоральных спецификаций на языке CTL могут быть представлены в разрешимом подмножестве зависимой системы типов.
Ключевые слова:
Постоянный URL
Статьи в номере
- ОСОБЕННОСТИ ПРОЕКТИРОВАНИЯ ДИФРАКЦИОННЫХ РЕШЕТОК
- АБЕРРАЦИОННЫЙ АНАЛИЗ КОМПОЗИЦИИ ТОНКОГО ОПТИЧЕСКОГО КОМПОНЕНТА С КОНЦЕНТРИЧЕСКИМ МЕНИСКОМ
- МОДЕРНИЗИРОВАННЫЙ КОМПЛЕКС СИНТЕЗА И ВОССТАНОВЛЕНИЯ ГОЛОГРАММ-ПРОЕКТОРОВ ФРЕНЕЛЯ
- МЕТОД ОПРЕДЕЛЕНИЯ ПРОСТРАНСТВЕННОГО ПОЛОЖЕНИЯ ОБЪЕКТА ВБЛИЗИ ВОДНОЙ ПОВЕРХНОСТИ
- ВРАЩАТЕЛЬНАЯ ЗАВИСИМОСТЬ РЕЗОНАНСОВ ТИПА КОРИОЛИСА И ФЕРМИ В МАЛЫХ ЛИНЕЙНЫХ МОЛЕКУЛАХ
- ИТЕРАЦИОННЫЕ МЕТОДЫ РЕШЕНИЯ ФАЗОВОЙ ПРОБЛЕМЫ В ОПТИКЕ И ИХ ОСОБЕННОСТИ
- ЛЮМИНЕСЦЕНЦИЯ МАРГАНЦА ВО ФТОРФОСФАТНЫХ СТЕКЛАХ
- АНАЛИЗ РОБАСТНОСТИ НЕАДАПТИВНОЙ СИСТЕМЫ УПРАВЛЕНИЯ ЭЛЕКТРОПРИВОДА C ВАРИАЦИЯМИ СТРУКТУРЫ И ПАРАМЕТРОВ
- СПЕКТРАЛЬНЫЙ АНАЛИЗ ДАННЫХ С АКСЕЛЕРОМЕТРОВ ДЛЯ ЗАДАЧ ОБНАРУЖЕНИЯ И ИДЕНТИФИКАЦИИ ТРАНСПОРТНЫХ СРЕДСТВ
- АНАЛИЗ ЛИНЕЙНЫХ СИСТЕМ С ПЕРЕМЕННЫМИ ПАРАМЕТРАМИ ДЛЯ СИНТЕЗА ИНТЕРВАЛЬНЫХ НАБЛЮДАТЕЛЕЙ
- МОДЕЛИРОВАНИЕ ПОЛЯ DVB-T В УСЛОВИЯХ ГОРОДСКОЙ ЗАСТРОЙКИ
- ПРИМЕНЕНИЕ ГЛУБИННЫХ ТРЕХКООРДИНАТНЫХ ДАТЧИКОВ НАКЛОНА ПРИ РЕШЕНИИ ЗАДАЧ ГЕОТЕХНИЧЕСКОГО МОНИТОРИНГА
- АЛГОРИТМ ОЦЕНКИ ОТНОШЕНИЯ СИГНАЛ/ШУМ РЕЧЕВЫХ СИГНАЛОВ
- МЕТОД ПОСТРОЕНИЯ УПРАВЛЯЮЩИХ АВТОМАТОВ НА ОСНОВЕ МУРАВЬИНЫХ АЛГОРИТМОВ
- ПРОГРАММИРОВАНИЕ ЗАДАЧ ВОССТАНОВЛЕНИЯ ИСКАЖЕННЫХ ИЗОБРАЖЕНИЙ НА C/C++ В СИГНАЛЬНЫХ МИКРОПРОЦЕССОРАХ ФИРМЫ TEXAS INSTRUMENTS
- КОНЕЧНО-АВТОМАТНАЯ РЕАЛИЗАЦИЯ ПОЛЬЗОВАТЕЛЬСКОГО ИНТЕРФЕЙСА ВСТРАИВАЕМОЙ СИСТЕМЫ НА ОСНОВЕ АСПЕКТНО-ОРИЕНТИРОВАННОГО ОПИСАНИЯ
- ГИСТОГРАММНАЯ НОРМАЛИЗАЦИЯ РЕЧЕВЫХ ПРИЗНАКОВ В ЗАДАЧЕ ВЕРИФИКАЦИИ ДИКТОРОВ
- СИСТЕМА ИДЕНТИФИКАЦИИ ВОЗРАСТНОЙ ГРУППЫ ГОВОРЯЩЕГО ПО ЗАПИСЯМ СПОНТАННОЙ РЕЧИ
- МЕТОД СБОРКИ КОНТИГОВ ГЕНОМНЫХ ПОСЛЕДОВАТЕЛЬНОСТЕЙ НА ОСНОВЕ СОВМЕСТНОГО ПРИМЕНЕНИЯ ГРАФОВ ДЕ БРЮИНА И ГРАФОВ ПЕРЕКРЫТИЙ
- ИССЛЕДОВАНИЕ ИТТРИЕВЫХ СВИНЦОВО-ФТОРИДНЫХ НАНОСТЕКЛОКЕРАМИК, АКТИВИРОВАННЫХ ИОНАМИ НЕОДИМА
- ПРОГРАММНЫЙ МОДУЛЬ ДЛЯ ОЦЕНКИ ПАРАМЕТРОВ ДИСПЕРСНЫХ СИСТЕМ ПО ИХ ИЗОБРАЖЕНИЯМ ДЛЯ КОЛИЧЕСТВЕННОГО ТРЕХМЕРНОГО СТЕРЕОАНАЛИЗА
- ВЛИЯНИЕ МОДИФИКАЦИИ ПОВЕРХНОСТИ НАПОЛНИТЕЛЯ НА СВОЙСТВА ЛАТЕКСНЫХ ПЛЕНОК
- ПРИНЦИПЫ ПОСТРОЕНИЯ ОТРАСЛЕВОЙ СИСТЕМЫ АВТОМАТИЗИРОВАННОГО ПРОЕКТИРОВАНИЯ В АВИАЦИОННОМ ПРИБОРОСТРОЕНИИ
- ВЫЧИСЛЕНИЕ МИНИМАЛЬНОГО ПО ДЛИНЕ ПУТИ ПРОВОДНИКА В ТОПОЛОГИЧЕСКОЙ ТРАССИРОВКЕ ПЕЧАТНОГО МОНТАЖА
- АЛГОРИТМ ОПРЕДЕЛЕНИЯ СПАМНОСТИ ДОКУМЕНТОВ НА ОСНОВЕ ФЕЙЕРОВСКИХ ОТОБРАЖЕНИЙ
- АНАЛИЗ СПОСОБОВ ИДЕНТИФИКАЦИИ ПОЛЬЗОВАТЕЛЯ В СЕТИ ИНТЕРНЕТ
- АЛГОРИТМ ДЕПЕРСОНАЛИЗАЦИИ ПЕРСОНАЛЬНЫХ ДАННЫХ
- АЛГОРИТМ ИДЕНТИФИКАЦИИ РЕКВИЗИТОВ ФИЗИЧЕСКИХ ЛИЦ В БАЗАХ ДАННЫХ НА ОСНОВЕ МЕТРИКИ ЛЕВЕНШТЕЙНА
- РАЗРАБОТКА ОНТОЛОГИИ ОТКРЫТЫХ ГОСУДАРСТВЕННЫХ ДАННЫХ НА ПРИМЕРЕ РАСХОДОВ БЮДЖЕТА САНКТ-ПЕТЕРБУРГА
- РЕНТГЕНОФАЗОВЫЙ АНАЛИЗ ИТТЕРБИЙ-ЭРБИЕВЫХ ОКСИФТОРИДНЫХ НАНОСТЕКЛОКЕРАМИК
- СПОСОБ РАСШИРЕНИЯ ФУНКЦИОНАЛЬНЫХ ВОЗМОЖНОСТЕЙ МОБИЛЬНОГО ТЕРМИНАЛА МОНИТОРИНГА ПОДВИЖНЫХ ОБЪЕКТОВ
- ИССЛЕДОВАНИЕ АВТОКОЛЛИМАЦИОННОЙ СИСТЕМЫ ИЗМЕРЕНИЯ УГЛОВЫХ ДЕФОРМАЦИЙ КРУПНОГАБАРИТНЫХ ОБЪЕКТОВ
- ЭКСПЕРИМЕНТАЛЬНОЕ ИССЛЕДОВАНИЕ ОПТИКО-ЭЛЕКТРОННОЙ СИСТЕМЫ ИЗМЕРЕНИЯ ДЕФОРМАЦИЙ ЭЛЕМЕНТОВ КОНСТРУКЦИИ РАДИОТЕЛЕСКОПА РТ70 (СУФФА)
- ОРГАНИЗАЦИЯ ПЛАНИРОВАНИЯ ДЕЯТЕЛЬНОСТИ ПРИБОРОСТРОИТЕЛЬНОГО ПРЕДПРИЯТИЯ ПРИ ПРОВЕДЕНИИ НАУЧНО-ИССЛЕДОВАТЕЛЬСКИХ И ОПЫТНО-КОНСТРУКТОРСКИХ РАБОТ В АВИАЦИОННОЙ ОТРАСЛИ
- СТЕРЕОСКОПИЧЕСКАЯ ОПТИКО-ЭЛЕКТРОННАЯ СИСТЕМА ДЕФОРМАЦИОННОГО МОНИТОРИНГА КРУПНОГАБАРИТНЫХ КУПОЛЬНЫХ КОНСТРУКЦИЙ