The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination


Цитировать

Полный текст

Открытый доступ Открытый доступ
Доступ закрыт Доступ предоставлен
Доступ закрыт Только для подписчиков

Аннотация

In the deductive verification of programs written in the imperative programming languages, the generation and proving of the verification conditions corresponding to loops are of particular complexity, as each of them must be provided with an invariant, whose construction is often a challenge. As a rule, the methods for the synthesis of loop invariants have a heuristic character, which complicates their application. An alternative is the symbolic loop invariant elimination method proposed by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in the form of a special replacement operation under certain constraints. Such an operation in the symbolic form expresses the loop effect, which allows introducing an inference rule for the loops without invariants into axiomatic semantics. This work is the further development of this method. It extends the proposed method of mixed axiomatic semantics for the verification of C-light programs. This extension incorporates the method for the verification of iterations over changeable arrays with the possible exit from the loop body in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule has been implemented in the verification condition generator, which is a part of the automated system for the verification of C-light programs. To perform automated verification in the used ACL2 system, two algorithms, one of which generates the replacement operation in the ACL2 language, and the second generates the auxiliary lemmas resulting in the successful automated proof of the obtained verification conditions in the ACL2 system have been developed and implemented. The application of the above mentioned methods and algorithms is illustrated with an example.

Об авторах

D. Kondratyev

Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences

Автор, ответственный за переписку.
Email: apple-66@mail.ru
Россия, Novosibirsk, 630090

I. Maryasov

Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences

Автор, ответственный за переписку.
Email: ivm@iis.nsk.su
Россия, Novosibirsk, 630090

V. Nepomniaschy

Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences

Автор, ответственный за переписку.
Email: vnep@iis.nsk.su
Россия, Novosibirsk, 630090

Дополнительные файлы

Доп. файлы
Действие
1. JATS XML

© Allerton Press, Inc., 2019

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

8. Субъект персональных данных вправе запретить своему оборудованию прием этих данных или ограничить прием этих данных. При отказе от получения таких данных или при ограничении приема данных некоторые функции Сайта могут работать некорректно. Субъект персональных данных обязуется сам настроить свое оборудование таким способом, чтобы оно обеспечивало адекватный его желаниям режим работы и уровень защиты данных файлов «cookie», Оператор не предоставляет технологических и правовых консультаций на темы подобного характера.

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

10. Я согласен/согласна квалифицировать в качестве своей простой электронной подписи под настоящим Согласием и под Политикой обработки персональных данных выполнение мною следующего действия на сайте: https://journals.rcsi.science/ нажатие мною на интерфейсе с текстом: «Сайт использует сервис «Яндекс.Метрика» (который использует файлы «cookie») на элемент с текстом «Принять и продолжить».