Event

Laboratory work uses Tina modeling system, mCRL2 (http: /projects.laas/fr/tina, https://www.mcrl2.org), modern open source software and models located in the GitHub.

The course presents a balance of theory and practice of software verification, including verification of parallel and distributed programs. These methods are the basis for the development of reliable (secure) software. Most information about the reliability of modern programs is based on testing methods that guarantee a certain probability of the program performing a given function. Formal proof of software correctness is the next step in improving the reliability of software for special applications in real-time systems, as well as in vital areas.

The goal of course is to form knowledge of basic terms and concepts of mathematical techniques and software verification; to study theoretical and practical foundations, principles and basic methods of software verification; as well as acquisition of practical skills to prove the correctness of applied algorithms, acquisition of skills which are necessary for further scientific and professional activities.

Topic 1. Tools for verification of serial and parallel programs written on algorithmic languages.

Topic 2.Verification of parallel software by Petri nets (PN).

Topic 3. Algebra and calculus of processes as verification technique of distributed programs.