ACSL By Example

Для тех, кто хочет познакомиться с языком формальной спецификации программ на языке Си, ACSL, выпущено пособие под названием "ACSL By Example" (ссылка для скачивания). Написав спецификацию к программе на Си, можно воспользоваться инструментом Frama-C с плагином Jessie для автоматического получения условий верификации, корректности и завершимости в синтаксисе, пригодном для применения ряда автоматических пруверов (например, Alt-Ergo, CVC3, Z3, Simplify и т.п.) и интерактивных пруверов (например, PVS).