RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2015, том 22, номер 6, страницы 763–772 (Mi mais472)  

Fast and safe concrete code execution for reinforcing static analysis and verification

[Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ]

M. Belyaev, V. Itsykson

Peter the Great St. Petersburg Polytechnic University, Polytechnicheskaya street, 21, Saint-Petersburg, 194021, Russia

Аннотация: Существующие средства и методы статического анализа и верификации кода на языке С используют различные методики упрощения программной модели, приводящие к значительному снижению точности анализа. В данной работе представлен новый подход к повышению точности анализа путем исполнения программной модели в контролируемом окружении, которое позволяет точно определять ошибочные ситуации, такие, как нарушения контрактов кода и ошибки работы с памятью, оставаясь при этом эффективным с точки зрения затрат по времени и по памяти. Данный подход был реализован в модуле под названием «Tassadar» в рамках средства ограниченной проверки моделей «Borealis». Прототип был опробован на стандартных наборах тестовых программ данного средства и показал минимальное влияние на его общую производительность.
Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.
Статья публикуется в авторской редакции.

Ключевые слова: программная интерпретация, символьное исполнение, статический анализ программного кода, точность анализа.

DOI: https://doi.org/10.18255/1818-1015-2015-6-763-772

Полный текст: PDF файл (486 kB)
Список литературы: PDF файл   HTML файл

Реферативные базы данных:

Тип публикации: Статья
УДК: 004.054+004.4'23
Поступила в редакцию: 15.09.2015
Язык публикации: английский

Образец цитирования: M. Belyaev, V. Itsykson, “Fast and safe concrete code execution for reinforcing static analysis and verification”, Модел. и анализ информ. систем, 22:6 (2015), 763–772

Цитирование в формате AMSBIB
\RBibitem{BelIts15}
\by M.~Belyaev, V.~Itsykson
\paper Fast and safe concrete code execution for~reinforcing static analysis and verification
\jour Модел. и анализ информ. систем
\yr 2015
\vol 22
\issue 6
\pages 763--772
\mathnet{http://mi.mathnet.ru/mais472}
\crossref{https://doi.org/10.18255/1818-1015-2015-6-763-772}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3493709}
\elib{http://elibrary.ru/item.asp?id=25125093}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais472
  • http://mi.mathnet.ru/rus/mais/v22/i6/p763

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:163
    Полный текст:68
    Литература:37
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020