Methods for analysis of data from social networks
This work focuses on the analysis of online social networking services. We examine several formal definitions of various characteristics (numerical and structural) and introduce appropriate concepts, models and methods that could be useful for the analysis of information obtained from social networks. Preference analysis is proposed to be used to...
Situation analysis for transport network development forecast in the MIX-PROSTOR system
The paper describes a system of scientific research automation applied to the forecasting of the development of Russian core transport network. The process of formation, evaluation and analysis of forecasted variants is considered. The variants can be combined, which allows for the implementation of the concept of the situation room...
Formal verification of programs for abstract register machines
Abstract register machines are an important formal model of computation widely used for the modeling of many classes of computational algorithms and the analysis of their complexity. Despite the significance of this model, formal verification of general-purpose programs for abstract register machines has not been properly covered in the existing...
ALC for CLA: Towards description logic on concept lattices
In this paper, we start with a motivation of the study of modal and/or description logics with values in concept lattices. Then we give a brief survey of approaches to lattice-valued modal and/or description logics. After that we study some methods of context symmetrization, because in our approach the description...
Constructions used in associative parallel algorithms for undirected graphs. Part 1
The paper selects constructions used to represent a group of algorithms for undirected graphs given as a list of edges and their weights on a model of associative (content addressable) parallel systems with vertical processing (the STAR–machine). To this end, the paper analyzes the implementation on the STAR–machine of classical...
Experiments on self-applicability in the C-light verification system
Development of the C-light verification system is accompanied by various case studies. We have already demonstrated the applicability of our system to some examples from verification competitions. Those programs are connected to verification-difficult issues but, as a rule, they are represented by artificial or trivial pieces of code. Now we...
Back-end translator for Sisal 3.1 compiler
Sisal is a single-assignment language without side effects. Sisal supports error values and a flow data type and allows recursion. It has a verbose syntax, which reminds that of Pascal in some cases. Sisal is positioned as a language for scientific computations, implicitly parallel and effective. It can significantly simplify...