## Context machines as formalism for specification of dynamic systems

An approach to the development of easy-to-use operational specifications of dynamic systems is presented. It is based on the formalism of context machines and the language of description of context machines CML. The main notions of the theory of context machines are defined. Classification of general-purpose contexts is suggested. The...

## An approach to visualization of knowledge portal content

The process of development of an ontology-based knowledge portal and creation of its content is time-consuming and labor-intensive. It is very desirable to have special analysis facilities for maintenance and development of such a portal. The subject of our paper is a tool for visual analysis of content and ontology...

## Timed transition systems with independence and timed event structures: an adjunction

The behaviour of concurrent systems is often specified extensionally by describing their “state-transitions” and the observable behaviours that such transitions produce. The simplest formal model of computation able to express naturally this idea is that of labelled transition systems, where the labels on the transitions represent the observable part of...

## On recognition of low quality texts

An acute problem for archives and museums is providing high-quality digitized text from low-quality or damaged originals. The majority of companies working in the field of optical character recognition (OCR) focus on digitzed texts of high quality, which represent the majority of processed data and the market for these companies’...

## Basic associative parallel algorithms for vertical processing systems

In this paper, by means of an abstract model of the SIMD type with vertical data processing (the STAR{machine), we present basic associative parallel algorithms. These algorithms are represented as the corresponding procedures for the STAR{machine, whose correctness is justified and the time complexity is evaluated. We also propose a...

## The uniform constraint solving API for UniCalc

The paper describes a programming interface that we have developed to separate constraints, solvers, and cooperation strategies in a constraint programming toolkit UniCalc. The interface is simple but it allows us to express such constraint solving techniques as increasing the level of consistency, various strategies for exhaustive search, and cooperation...

## The problems of C program verification

The fully automatic verification of programs is a tempting and hardly accessible goal of modern programming. The low-level nature of the most popular programming languages, such as C and C+, has raised its difficulty to a new level. New formal methods and specification languages are required, because the classical Hoare...

## The language of calculus of computable predicates as a minimal kernel for functional languages

Logical semantics is a new kind of formal semantics used to describe semantics of pure call-by-value functional languages. For the statement S, the logical semantics LS(S) is a predicate that is true for the variable values for which the execution of S is finished. Let a specification of the statement...

## Fabulous arrays I: Operational and transformational semantics of static arrays in verification project F@BOOL@

The purpose of the F@BOOL@ project is to develop a transparent for users, compact, portable and extensible verifying compiler F@BOOL@ for annotated computer programs, that uses effective and sound automatic programs for checking satisfiability of propositional Boolean formulas. The kernel programming language of the project interprets all variables by residuals...

## Implementation of the algorithm of hierarchical cluster analysis on GPU by means of CUDA technology

In the paper, the algorithm of the hierarchical cluster analysis is considered and the method is proposed to transfer this algorithm onto the parallel multiprocessor system used on modern graphics processing units (GPUs). Within the frameworks of some natural assumptions, we have estimated the run time of the algorithm in...