2023/2024

Automated Methods for Program Verification

Type: Mago-Lego

Delivered by: School of Data Analysis and Artificial Intelligence

When: 1, 2 module

Open to: students of all HSE University campuses

Language: English

ECTS credits: 6

Contact hours: 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.