# Today's number

Today's numberCurrent number (#№ 15, 2019)

Download full number (3.92 MB)

## System Description: Russell - A Logical Framework for Deductive Systems

Russell is a logical framework for the specification and implementation of deductive systems. It is a high-level language with respect to Metamath language, so inherently it uses a Metamath foundations, i.e. it doesn't rely on any particular formal calculus, but rather is a pure logical framework. The main difference with Metamath is in the proof language and approach to syntax: the proofs have a declarative form, i.e. consist of actual expressions, which are used in proofs, while syntactic grammar rules are separated from the meaningful rules of inference.
Russell is implemented in c++14 and is distributed under GPL v3 license. The repository contains translators from Metamath to Russell and back. Original Metamath theorem base (almost 30 000 theorems) can be translated to Russell, verified, translated back to Metamath and verified with the original Metamath verifier. Russell can be downloaded from the repository: https://github.com/dmitry-vlasov/russell.

## A Method to Verify Parallel and Distributed Software in C# by Doing Roslyn AST Transformation to a Promela Model

In this paper, we describe an approach to formal verification of parallel and distributive programs in C#. We use Microsoft Roslyn technique to get syntax and semantic information about interesting constructions in the real source code to generate some corresponding code in Promela language, designed to model actor-based interoperation systems, so we do a program-to-model transformation. Then, we verify the usual problems of parallel and distributive code by checking pre-defined LTL formulas for the model program. We are able to provide checking of data races, improper locking usage, possible deadlocks in distributive service interoperations using the Model Checking approach. This method can be used to construct a static analyzer for the .NET platform.

## Deductive verification of predicate program of binary search of an arbitrary type object

Development and deductive verification of a predicate program of binary search, which is identical to bsearch.c program in the Linux kernel library, is described. New constructs in the predicate programming language for arbitrary types as program parameters are introduced. For an object of the arbitrary type, the transformation of coding an object via pointer is introduced.

## Thematic Clusters within Text Sets and Examining Temporal Dynamics of Themes (Using Conference Proceedings in "Argument Mining")

This paper presents the results of examining changes that occur in thematic clusters constructed on a text set of conference proceedings from the research field "Argument mining".
Identification of terms, analysis of their relations and thematic clustering are performed with the use of a third-party software that allows to extract terms in the form of noun phrases and to cluster them in accordance to a modularity based algorithm. The quality of the resulting clusters is estimated by employing three distinct criteria. Temporal transformation of terminological content of clusters is analyzed through the use of directed graphs constructed with an underlying criterion that enables recognition of the most significant changes. Terminological lexicon of the identified thematic clusters characterizes distinct directions in which studies are conducted, while transformation of their terminological content demonstrates shifts of researchers' interests.

Ontological Approach to Organizing Specification Patterns in the Framework of Support System for Formal Verification of Distributed Program Systems
Ontological Approach to Organizing Specification Patterns in the Framework of Support System for Formal Verification of Distributed Program Systems
(p. 111-132)

The article describes the structure of the ontology of specification patterns from the texts of technical documentation. This ontology combines patterns of known classifications of requirements with new patterns. The ontology allows the recording of Boolean pattern combinations of the following types: qualitative, real and branching time, with combined events, quantitative characteristics of events and patterns, and simple statements about the data. Examples of the requirement patterns for the real vacuum control system of the Large Solar Vacuum Telescope are given. The scheme of intellectual support system for formal verification of distributed program systems is outlined.