Computer Science, № 31, 2010

The Atoment language is a domain-specific language of development for program verification methods. It is used in the multilanguage software system Spectrum of rapid development and testing of verification methods. The easy-to-use specialized language allows a user of the system to describe verification methods in a natural notation, verify algorithms...

The process of development of an ontology-based knowledge portal and creation of its content is time-consuming and laborious. The lifetime of such portals is sufficiently long and they collect a great volume of valuable information. This information can be analyzed from various points of view. This paper describes an extension...

In the paper, we give an overview of several approaches that we use to analyze “spam” (undesired bulk advertising) and the credentials of senders of spam, for the purpose of automatic detection. We use some of these approaches for discrimination between stolen account credentials and “spam-bots” (accounts opened purely for...

In this paper we use compositional methods for construction of a characteristic formula for the timed testing preorder in a model of timed event structures with discrete internal actions.

Timed transition systems are a widely studied model for real-time systems. In this work we deal with an extension of this model, timed transition systems with invariants. The intention of the paper is to show applicability of the general categorical framework of open maps in order to treat the decidability...

This work is dedicated to an actual problem of efficient information search in the Internet. The work is based on the algorithms of sentences comparison taking into account the schemes of syntactic analysis generated by Link Grammar Parser software. The main idea is that syntactic diagrams give us a primitive...

In the last 5 years, multi-core processors become more and more available to the wide public. Support for multi-core processors becomes de facto a standard for computation-intensive applications. In this paper, we present a parallel implementation of the UniCalc solver for non-linear engineering problems. Unlike the existent solvers of non-linear...

The classical Hoare logic links separate verification conditions (VCs) to linear paths of a program. The real verification condition generators (VCG) link VCs to line numbers at best. It can be insufficient, since VCs contain information neither about the evaluation order nor about correspondence between their fragments and specific operations...

A verifying compiler is a system program that translates programs written by an user from a high-level language into equivalent executable programs, and besides, proves (verifies) mathematical statements specified by the human about the properties of the programs being translated. The purpose of the F@BOOL@ project is to develop a...

For a discrete time stochastic extension dtsPBC of finite Petri box calculus (PBC) enriched with iteration, we define a number of stochastic equivalences. They allow one to identify processes with similar behaviour which are differentiated by the too discriminate semantic equivalence of the calculus. We investigate which is the weakest...

Time Petri nets with priorities are a widely studied model for real-time systems. The intention of the paper is to develop an algorithm for parametric timing behaviour verification of real-time and concurrent systems represented by prioritized time Petri nets (PrTPNs). To achieve the purpose, we introduce a notion of the...

The paper presents an approach to development of a system that supports decision-making for tasks aimed to reduce power consumption and enhance the environmental safety of a large-scale enterprise with a complex technological infrastructure. The architecture and operating principles of this system are discussed. Adjustment of the system to the...