Integrated approach to analysis and verification of imperative programs

This paper describes a new approach to the analysis and verification of imperative programs, which allows us to integrate, unify and combine the methods and techniques of analysis and verification of imperative programs, accumulate and use knowledge about them. A feature of the approach is to use the domain-specific language...

anureev.pdf176.35 KB

Visualization of citation networks for large science portals

We examine a number of methods for probing and understanding a large-scale structure of networks that evolve over time. In particular, we focus on citation networks, networks of references between documents such as research papers. We describe three different methods of visualization: the first is based on a hierarchical edge...

apanovich.pdf2.14 MB

Specification and verification of the classical sliding window protocol

We consider the well-known Sliding Window Protocol (SWP) which provides reliable and efficient transmission of data over unreliable channels. It seems quite important to give a formal proof of correctness for the SWP, especially because the high degree of parallelism in this protocol creates a significant potential for errors. However...

chkliaev.pdf215.29 KB

Properties of nonlinear systems and convergence of the Newton-Raphson method in geometric constraint solving

The paper describes an application of a variant of the Newton-Raphson method to solution of geometric constraint problems. Sparsity and rank deficiency of the corresponding nonlinear systems are emphasized and statistical data are presented. Several ways of handling underdeterminancy and overdeterminancy in solving the Newton linear systems are considered. The...

gatilovr.pdf122.77 KB

Memory organization with parallel access to information and its application for image processing

In this paper, a computer memory system intended for storing an arbitrary sequence of multidimensional arrays is described. This memory system permits parallel access to the cuts distinguished in a given array by fixing one of the coordinates and to a large set of parallelepipeds which are the same dimension...

glodovski.pdf440.64 KB

Make formal semantics easy and useful

We start with a “make easy” approach to popularize formal semantics for software engineers. It is based upon a toy language with “exoteric” operational, denotational and axiomatic semantics. Then we present a realistic and practical operational, denotational and axiomatic semantics for a simple programming language. We hope that our approach...

shilov.pdf429.8 KB

Performance evaluation of the generalized shared memory system in dtsPBC

The algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC) enriched with iteration. In this paper, a method of modeling and performance evaluation of concurrent systems in dtsPBC is outlined based on the stationary behaviour analysis. The method is then applied to the generalized shared...

tarasyuk.pdf227.72 KB