Введение в формальную верификацию с помощью SPARK

Описание

Узнайте, как доказать безопасность и надежность встроенного и системного программного обеспечения с помощью SPARK Pro, и посмотрите, как SPARK можно применить к марсоходу M.A.R.S. для доказательства его безопасности.
Узнайте все о языке SPARK Pro от эксперта AdaCore по SPARK, главы продукта и инноваций Тони Айелло.
На этом вебинаре 18 июня Тони расскажет:
Что такое SPARK?Доказательная верификация программ для языка SPARK - язык, производный от Ada, с широким охватом функциональности Ada.
Практическая, модульная, масштабируемая верификация для систем и встроенных программ.
Профессиональные, промышленные формальные методы.
Каково использовать SPARK?
Создание монитора безопасности для марсохода M.A.R.S.
Автоматическое доказательство для автономного режима.Обнаружение ошибки в режиме дистанционного управления.
Будущее:
SPARK и генеративный ИИ.SPARK:
лучший язык для использования в генеративном ИИ.

Автор

Сергей Киркоров