Верификация Си-программ: объяснение условий корректности и стандартная библиотека


https://doi.org/10.18255/1818-1015-2011-4-157-167

Полный текст:


Аннотация

Представлены два направления развития проекта по верификации Си-программ, разрабатываемого в ИСИ СО РАН. Во-первых, аксиоматическая семантика языка C-kernel была расширена семантической разметкой. Метки, выводимые непосредственно исчислением Хоара, соответствуют различным аспектам условий корректности (УК). Эти метки могут быть извлечены из термов и преобразованы в пояснения на естественном языке. Пояснения, понятные обычному пользователю системы верификации, могут быть полезны для понимания УК и локализации ошибок. Во-вторых, было специфицировано подмножество стандартной библиотеки языка Си. Спецификации написаны на языке ACSL и соответствуют модели памяти языка C-light. В работе представлены примеры использования этих двух подходов.

Об авторе

Алексей Владимирович Промский
Институт систем информатики имени А.П. Ершова СО РАН
Россия


Список литературы

1. Baudin P., Filliatre J.C., Marche C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language <http://www.frama-c.cea.fr/download/acsl_1.4.pdf>

2. Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. TPHOLs 2009. LNCS. 2009. Vol. 5674. P. 23-42.

3. Denney E., Fischer B. Explaining Verification Conditions // Proc. AMAST 2008. LNCS. 2008. Vol. 5140. P. 145-159.

4. Filliatre J.C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15-29.

5. Fraer R. Tracing the origins of verification conditions. Rocquencourt, 1996. 17 p. (Rapp. / INRIA; N 2840).

6. Leino K.R.M., Millstein T., Saxe J.B. Generating error traces from verification condition counterexamples // Science of Computer Programming. 2005. Vol. 55, N 1-3. P. 209-226.

7. Nepomniaschy V.A., Anureev I.S., Mikhailov I.N., Promsky A.V. Towards verification of C programs. C-Light language and its formal semantics // Programming and Computer Software. 2002. Vol. 28(6). P. 314-323.

8. Nepomniaschy V.A., Anureev I.S., Promsky A.V. Towards verification of C programs: Axiomatic semantics of the C-kernel language // Programming and Computer Software. 2003. Vol. 29(6). P. 338-350.

9. Promsky A.V. Towards C-light program verification: Overcoming the obstacles // Proc. PU-2009, 19-23 June, Altai Mountains, Russia, 2009. P. 53-63.

10. Promsky A.V. Error-tracing semantics for C-kernel // Bull. Nov. Comp. Center, Comp. Science. 2010. 31. P. 123-138.


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

Для цитирования: Промский А.В. Верификация Си-программ: объяснение условий корректности и стандартная библиотека. Моделирование и анализ информационных систем. 2011;18(4):157-167. https://doi.org/10.18255/1818-1015-2011-4-157-167

For citation: Promsky A.V. C Program Verification: VC Explanation and the Standard Library. Modeling and Analysis of Information Systems. 2011;18(4):157-167. (In Russ.) https://doi.org/10.18255/1818-1015-2011-4-157-167

Просмотров: 3

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)