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