Computer Science, № 32, 2011

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...

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...

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...

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...

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...

The paper proposes an efficient associative algorithm for dynamic update of the shortest paths tree of a directed weighted graph after deletion of an edge. To this end, we use the STAR–machine that simulates the run of associative (content addressable) parallel systems of the SIMD type with bit–serial (vertical) processing...

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...

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...