2023/2024
Методы автоматической верификации программ
Статус:
Маго-лего
Когда читается:
1, 2 модуль
Охват аудитории:
для всех кампусов НИУ ВШЭ
Язык:
английский
Кредиты:
6
Контактные часы:
50
Course Syllabus
Abstract
The course acts as introduction to some of the most successful logic based concepts, tools and techniques used today in CS and IT, which are behind a major breakthrough in the practical applications in verification of systems and software. These methods are proven to be of great theoretical and practical potential in CS and IT. The topics of this course fall under the umbrella of what is called verification (a) Verification means to verify that a system satisfies some property. (b) The system can be a physical or software system. (c) The property is expressed using specifications within a certain logical language. The course has been designed in accordance with the most recent trends in the program verification. The challenge has been twofold: (1) to select the material and design the course so that to make it meet the actual needs of the CS applications, and (2) to do that so that to allow the students to learn and digest all necessary ideas to efficiently prove that the programs behave in the correct way.