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