Introduction to the Atoment language
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...
An extension of a visualization component of ontology based portals with visual analytics facilities
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...
Models and algorithms for detection of spam and senders of spam
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...
Compositional methods in characterization of timed event structures
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.
The timed barbed bisimulation is decidable for timed transition systems with invariants
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...
Methods of syntactic analysis and comparison of constructions of a natural language oriented to use in search systems
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...
Scalable parallel subdefinite calculations for sparse systems of constraints
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...
Error-tracing axiomatic semantics for C-kernel
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...
Guided tour inside F@BOOL@: a case-study for a SAT-based verifying compiler
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...
Performance preserving equivalences for dtsPBC
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...
Real arithmetic based verification of prioritized time Petri nets with parameters
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...
An approach to development of the decision support system for enterprise with complex technological infrastructure
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...