The problems of program modeling based on program semantics and program verification are central to modern computer science and the development of correct, reliable and secure software and hardware. In its most general form, the problem of modeling of formal semantics is to build mathematical objects that correspond to programs, and the problem of verification is to build a mathematical proof of the proposition that a program satisfies its requirements on the base of a given formal semantics. Requirements for programs can reflect aspects of their execution, for example, one class of requirements is that the program correctly calculates a given function, another class of requirements expresses security properties (for example, the absence of unauthorized information leaks during the program execution), the third class of requirements expresses program reliability (i.e., its ability to remain operational in emergency situations), etc.
To verify various classes of programs, mathematical models of formal semantics and verification methods and algorithms based on these models have been developed. The course will present the most widely used formal semantics: operational, denotational, logical. The classes of program models will be described and the corresponding verification algorithms described. The course will be devoted to classical methods of program verification - the Floyd method, temporal logic and Model Checking verification method, structural induction and computational induction verification of functional programs, as well as methods based on the process theory. The presentation of mathematical models and methods of program verification will be supported by the study of practical verification systems.
- Teacher: Andrei Mironov
- Teacher: Nikolay Vasilev