Описание:Изучаются математические методы проверки корректности поведения программ, включая методы верификации программ при помощи логики Хоара и метод верификации моделей программ (model checking). Рассматриваются и обосновываются основные приемы построения моделей программ, логические средства спецификации их поведения, а также алгоритмы проверки выполнимости спецификаций на заданных моделях схем. Изучаются инструментальные средства верификации моделей для темпоральных логик NuSMV (Symbolic Model Verifier) и SPIN и их применение для верификации моделей программ.