Download presentation

Yuri Karpov

Professor Yuri Karpov, PhD, member of the American Mathematical Society since 1975, expert in Russian research and technology field. Dr. Karpov professional interests include problems of parallel processes formal models, distributed systems modeling and analysis, and verification of distributed and parallel algorithms.

Dr. Karpov’s professional experience included consultancy work for Hewlett-Packard, where he specialized in formal analysis and communication protocols verification; he was also in charge of several research projects for HP labs Europe and IBM Centre for Advance Studies.

In 1999 he became invited professor of the Institute of Parallel and Distributed Systems at the University of Stuttgart (Germany). Together with A.V.Borschevoi and V.Rudakov, Dr. Karpov founded XJ Technologies software company and became its President.

Dr. Karpov has been the Head of Distributed Computing and Networking Department of St. Petersburg State Technical University since 1995 when it was founded. He teaches Mathematical Logic and Algorithm Theory, Automata and Formal Languages Theory, Distributed Algorithms and Protocols, Parallel and Distributed Program Systems Verification.

Dr. Karpov is the author of over 150 academic papers and several books, including “Automata Theory”, “Programming theory and technology. Building compiler fundamentals”, “The imitation modeling. Introduction to modeling with AnyLogic 5”, “Model checking. Verification of parallel and distributed software systems”.

Presentation: On the way to practical application of verification in the process of software system development

Yuri Karpov, Irina Shoshmina

Universal, ubiquitous computerization of all aspects of life makes a person more vulnerable and dependent on technology he created. That’s why the achievement of the required quality of software systems for critical applications is becoming an important scientific and technical challenge.

Software verification has a great potential in solving this problem. Verification is a formal check of the compliance with formal requirements to the program system behavior, presented as a formal model.

A recent breakthrough on verification studies is associated with the Model checking method. Method is based on the fact that the truth of temporal logic formula, describing program behavior requirements is checked on a program model.

The theory and algorithms of Model checking are sufficiently developed, and there are some impressive examples of successful model applications, but accordingly to Geoffrey Moore’s classification, verification is still used by “innovators” and “technology enthusiasts” only. Meanwhile, the reports on breakdowns of technical systems caused by software errors continue to terrify society. Presentation examines the challenges of implementing the verification phase into technological cycle of programming.