Магистратура
2021/2022
Методы автоматической верификации программ
Статус:
Курс по выбору (Науки о данных (Data Science))
Направление:
01.04.02. Прикладная математика и информатика
Где читается:
Факультет компьютерных наук
Когда читается:
1-й курс, 1, 2 модуль
Формат изучения:
без онлайн-курса
Охват аудитории:
для всех кампусов НИУ ВШЭ
Преподаватели:
Канович Макс Иосифович
Прогр. обучения:
Науки о данных
Язык:
английский
Кредиты:
4
Контактные часы:
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.
Learning Objectives
- To introduce students to techniques behind most impressive verification tools, which are based on <i> Hoare logics and <i> SAT solving.</i></i>
- To cover <i> symbolic model checking and <i> symbolic execution.</i></i>
Expected Learning Outcomes
- Apply Conflict-Driven Clause Learning as an efficient tool for SAT solving in practice.
- Formal definition of interpretation of predicate logic domain (universe and interpretation of symbols).
- Formal description of predicate logic syntax.
- Get a big picture on the materials to be covered by the course.
- Informal description of predicate logic formulas semantics, including connectives and quantifiers.
- Introduced to reasoning about predicate logic formulas.
- Learn bound and free variables.
- Learn formal semantics of predicate logic.
- Learn semantics of predicate logic with ensuring its orientation to the actual needs of computer science and information technology.
- Learn syntax and semantics of predicate logic with ensuring its orientation to the actual needs of computer science and information technology.
- Learn validity, satisifiability, etc.
- Learning the basic of software verification using SAT solvers.
- Manually run symbolic execution rules for loop-free programs.
- Software verification using SAT solvers.
- Specify programs formally using Hoare triples.
- Understand an algorithm for generating loop invariants automatically.
- Understand how to translate programs into SAT.
- Understand the aim of the course.
- Understand the definition of loop invariants.
- Understanding SAT solvers.
- Understanding the DPLL algorithm.
- Understanding the importance of distinguishing syntax and semantics.
- Use symbolic execution rules to prove loop-free programs semi-automatically.
Course Contents
- Introduction to the course and basic concepts of verification
- Basic concepts of propositional logic
- Predicate logic as a language for CS
- Semantics of Predicate Logic
- Hoare Triples <i>{P(x, y, z)} c {Q(x, y, z)}</i>
- Hoare Logic: Inference Rules
- Symbolic Execution
- Hoare Logic and Symbolic Execution
- Automatic Inference of Loop Invariants
- SAT Solvers
- SAT Solvers, Symbolic model checking
- Software verification using SAT solvers
