Программы

Набор инструментов Astraver состоит из платформы для анализа исходного кода Frama-C, платформы для дедуктивной верификации Why3 и плагина Jessie.

В рамках проекта Astraver создан форк плагина Jessie под названием Jessie2. Он позволяет осуществлять дедуктивную верификацию программ на языке C с аннотациями на языке ACSL и использует язык и инструменты платформы Why3. Jessie2 не привязан к платформе Why2, в отличие от оригинального Jessie, и может быть установлен отдельно.

Страница разработки данного набора инструментов находится на сайте проектов с открытым исходным кодом ИСП РАН - forge.ispras.ru. В разделе "руководства" вы также можете ознакомиться с руководством по установке инструментов.

Для верификации больших объемов кода также могут быть полезны вспомогательные инструменты, созданные в рамках проекта Astraver. Страница разработки этих утилит также находится на forge.ispras.ru.