Сборники трудов ИСП РАН


Автоматическое доказательство безопасности локальных пустых указателей

А.В. Когтенков (ETH, Цюрих, Швейцария)

Аннотация

Разыменование пустого указателя – это хорошо известная ошибка, встречающаяся в объектно-ориентированных программах. Ее можно избежать путем добавления к языку, на котором пишется программа, специальных правил приложимости. Достаточно ли этих правил для гарантии отсутствия таких исключительных ситуаций? Данная статья посвящена безопасности пустых указателей во внутрипроцедурном контексте, в котором не требуются какие-либо дополнительные аннотации. Правила формализуются в системе автоматического доказательства теорем Isabelle/HOL. Затем доказывается теорема о сохранении безопасности пустых указателей в крупношаговой семантике. Наконец, демонстрируется, что при наличии таких правил семантики с безопасностью пустых указателей и без нее эквивалентны.

Ключевые слова

безопасность пустых указателей, статический анализ, Eiffel, формальные методы, крупношаговая операционная семантика, теорема о сохранении, эквивалентность операционных семантик

Издание

Труды Института системного программирования РАН, том 28, вып. 5, 2016, стр. 27-54.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(5)-2

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома