Описание:Рассматриваются фундаментальные вопросы формальных моделей вычислений и утверждения, ограничивающие применимость методов формальной верификации. Слушатели получат представление о теоретических основаниях дедуктивных методов формальной верификации программ на примере разновидностей типизированного λ-исчисления.