Formal Specification and Verification of Programs
The course focuses on the problems of development of mission-critical program system. Special stress is being placed on the formalization of the functional properties of the systems and analytical verification methods. Students will get acquainted with modern approaches and tools for verification of programs in object-oriented and system programming languages. The course includes participation in lectures, seminars and practical training on different methods of formal specification of the program properties using specification languages RAISE, Spec #, Dafny, ACSL and also analytical verification using such tools as Dafny, Frama-C and PVS.
More information can be found here.