arXiv subjects
Publications and source records attributed to Andrew M. Mironov.
This paper presents a new, significantly simpler proof of one of the main results of applied pi-calculus: the theorem that the concepts of observational and labeled equivalence of extended processes in applied pi-calculus coincide.
In this paper, we outline an approach to verifying parallel programs. A new mathematical model of parallel programs is introduced. The introduced model is illustrated by the verification of the matrix multiplication MPI program.
Cryptographic Protocols (CP) are distributed algorithms intended for secure communication in an insecure environment. They are used, for example, in electronic payments, electronic voting procedures, systems of confidential data processing, etc. Errors in CPs can bring to great financial and social damage, therefore it is necessary to use mathematical methods to substantiate the correctness and safety of CPs. In this paper, a distributed process model of CPs is presented, which allows one to formally describe CPs and their properties. It is shown how to solve the problems of verification of CPs on the base of this model.
In the paper we introduce graphical objects (called state diagrams) related to functional programs. It is shown that state diagrams of functional programs can be used to solve problems of verification of functional programs. The proposed approach is illustrated by an example of verification of a sorting program.
In the paper we consider a graph model of message passing processes and present a method verification of message passing processes. The method is illustrated by an example of a verification of sliding window protocol.
In the paper we introduce a process model of security protocols, where processes are graphs with edges labelled by actions, and present a new method of specification and verification of security protocols based on this model.
In the paper the problem of verification of functional programs (FPs) over strings is considered, where specifications of properties of FPs are defined by other FPs, and a FP S1 meets a specification defined by another FP S2 iff a composition of functions defined by the FPs S1 and S2 is equal to the constant 1. We introduce a concept of a state diagram of a FP, and reduce the verification problem to the problem of an analysis of the state diagrams of FPs. The proposed approach is illustrated by the example of verification of a sorting program.
In the book we present main concepts of probabilistic automata theory.
The book gives a detailed exposition of basic concepts and results of a theory of processes. The presentation of theoretical concepts and results is accompanied with illustrations of their application to solving various problems of verification of processes. Along with well-known results there are presented author's results related to verification of processes with message passing, and there are given examples of an application of these results.