Проект посвящен изучению языка спецификаций ACSL, определению операций языка С (например, битовых операций сдвига << и >>), для которых вопрос написания спецификаций требует, на текущий момент, дополнительной проработки, формированию аксиоматической теории для написания ACSL-спецификаций отдельных операций языка С, обеспечивающей их верификацию с помощью Frama-C и плагина WP. Доказать выполнение условий с применением Frama-С в общем случае нельзя. Необходимо реализовать аксиоматическую теорию...Подробнее

Исследование возможности повышения уровня автоматизации верификации ACSL-спецификаций для отдельных операций языка С

Демонстрация результатов выполнения задач, поставленных в Wekan, руководителю проекта и представителям заказчика

Демонстрация возможностей модуля, поддерживающего предложенные аксиоматические теорий

Средства разработки на Caml, С++/Python

1. Теория axiomatic Index_of_item, с.5 в работе [loulergue_bk_tap_2018.pdf] 2. Теория axiomatic StrnCmp в проекте https://github.com/evdenis/verker/blob/master/src/strncmp.h