На первый взгляд верификация программ – это надежный метод, что гарантируется ее проработанной формальной базой. Однако она работает без проблем только в идеальном случае, когда программа и ее спецификация корректны, теория проблемной области полна и доказатель теоремы достаточно мощный. При нарушении любого из этих требований верификация значительно усложняется. Помимо возможных проблем в формальных основах (не рассматриваются в данной работе) причиной может быть то, что верификация, как процесс, по-прежнему использует неформальные или полуформальные методы. К ним относится локализация ошибок. Данная работа является обзором методов локализации/объяснения ошибок, разработанных в проекте C-light для решения этой проблемы. Их применение показано на примерах.
- Новости
- Институт
- Выборы директора
- Основная информация
- А.П. Ершов
- История
- Структура института
- Сотрудники
- Ученый совет
- Диссертационный совет
- Сведения об образовательной организации
- Профком ИСИ
- Адрес
- Телефонный справочник, PDF
- ИСИ СО РАН в прессе
- Международное сотрудничество
- Годовые отчеты
- Фотоархив ИСИ
- Видеоархив ИСИ
- Полезные ссылки
- Реквизиты
- Вакансии
- Документы
- Обучение
- Проекты
- Публикации
- О публикациях
- Список публикаций
- Препринты
- Авторефераты
- Сборники статей
- Книги сотрудников ИСИ
- Учебные и методические пособия
- Зарубежные публикации
- Методика определения импакт-фактора научного журнала
- Научно-популярные статьи сотрудников ИСИ в прессе
- ГОСТ Р 7.0.11-2011 - Диссертация и автореферат диссертации
- Как правильно оформлять список литературы
- Рекомендации по подготовке и оформлению статей
- Экспертизы публикаций
- Издания ИСИ
- Конференции
- Библиотека