### ?

## Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science

Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.
Cham :
Springer, 2017.

Under the general editorship: O. Strichman, R. Tzoref-Brill

This book constitutes the refereed proceedings of the 13th International Haifa Verification Conference, HVC 2017, held in Haifa, Israel in November 2017. The 13 revised full papers presented together with 4 poster and 5 tool demo papers were carefully reviewed and selected from 45 submissions. They are dedicated to advance the state of the art and state of the practice in verification and testing and are discussing future directions of testing and verification for hardware, software, and complex hybrid systems.

Tatarnikov A., Kamkin A., Чупилко М. М. et al., , in : Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science. Vol. 10629: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017.: Cham : Springer, 2017. P. 217-220.

The paper presents MicroTESK, a tool that automates construction of test program generators for microprocessors. A constructed generator consists of the core that implements architecture-independent generation methods and the model that holds information required to generate tests for the corresponding architecture. The tool extracts this information from formal specifications of the instruction set architecture. The ...

Added: January 24, 2018

Springer, 2018

This book constitutes the refereed proceedings of the 4th International Conference on Tools and Methods for Program Analysis, TMPA 2017, Moscow, Russia, March 3-4, 2017.
The 12 revised full papers and 5 revised short papers presented together with three abstracts of keynote talks were carefully reviewed and selected from 51 submissions. The papers deal with topics such as ...

Added: November 12, 2018

Zakharov V., Темербекова Г. Г., Моделирование и анализ информационных систем 2016 Т. 23 № 6 С. 741-753

Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In ...

Added: October 13, 2016

Smeliansky R. L., Chemeritsky E. V., Zakharov V., Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398-406

Software-dened networking (SDN) is an approach to building computer net- works that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and ow-table updating was dened in the form of a protocol known ...

Added: September 30, 2015

Zakharov V., Temerbekova G., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 523-530

Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In ...

Added: October 13, 2016

Zakharov V., Труды Института системного программирования РАН 2015 Т. 27 № 2 С. 221-250

Finite state transducers extend the finite state automata to model functions on strings or lists. They may be used also as simple models of sequential reactive programs. These programs operate in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data such program performs a sequence of actions. ...

Added: September 30, 2015

Smetanin S., Ometov A., Komarov M. M. et al., Sensors 2020 No. 12 P. 3358

The present increase of attention toward blockchain-based systems is currently reaching a tipping point with the corporate focus shifting from exploring the technology potential to creating Distributed Ledger Technology (DLT)-based systems. In light of a significant number of already existing blockchain applications driven by the Internet of Things (IoT) evolution, the developers are still facing ...

Added: June 15, 2020

Zakharov V., Temerbekova G., Системная информатика 2016 No. 7 P. 33-44

Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In some cases verification of such programs can be reduced to minimization and equivalence checking problems for this model of computation. To solve efficiently these problems certain requirements are imposed on a semigroup these transducers operate on. Minimization of ...

Added: October 13, 2016

Berlin : Springer, 2014

This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 ...

Added: July 3, 2014

Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506-524

One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a ﬁnite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between ﬂows of control signals ...

Added: October 26, 2018

Kamkin A., М. : МАКС Пресс, 2018

This textbook is devoted to formal methods for program verification and is based on the lectures given by the author at CMC MSU, DCAM MIPT, and FCS HSE. It describes the basics of such approaches as deductive analysis and model checking. The list of topics includes formal semantics of programming languages (operational and axiomatic semantics), ...

Added: November 2, 2018

Zakharov V.A., Lecture Notes in Computer Science 2015 Vol. 9270 P. 208-221

Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In this paper we introduce a uniform tech- nique for checking eectively functionality, k-valuedness, equivalence and inclusion for this model of computation in the case when a semigroup these transducers op- erate over is embeddable in a decidable group. ...

Added: September 30, 2015

Gnatenko A., Zakharov V., Системная информатика 2020 Vol. 17 P. 21-32

Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop ...

Added: November 9, 2020

Gnatenko A., Zakharov V., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663-675

One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...

Added: October 17, 2019

Switzerland : Springer, 2017

This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017.
The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, ...

Added: May 6, 2017

Gnatenko A., Zakharov V., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303-324

The syntax and semantics of the new temporal logic LP-CTL * designed for the formal specification of the behavior of sequential responsive programs, modeled by automata-transducers (transducers) over semigroups, are developed. An algorithm is developed for verifying the feasibility of the formulas of the proposed temporal logic on models represented by finite transducers working on ...

Added: June 14, 2018

М. : National Instruments Russia, 2017

Содержание сборника составляют доклады с результатами оригинальных исследований и технических решений, ранее не публиковавшиеся. Мы надеемся, что предлагаемый сборник окажется полезным для специалистов, работающих в различных областях науки и техники, для широкого круга преподавателей, аспирантов и студентов ВУЗов, а также для преподавателей средних школ и технических колледжей. ...

Added: May 10, 2017

Karpov V. E., Karpova I. P., Procedia Engineering 2015 Vol. 100 P. 1459-1468

Work solutions are proposed for problems of leader definition and role distribution in homogeneous groups of robots. It is shown that transition from a swarm to a collective of robots with hierarchical organization is possible using exclusively local interaction. The local revoting algorithm is central to the procedure for choice of leader while redistribution of roles can ...

Added: March 14, 2015

Chernyshev S. V., Cherepanov E. A., Pankratiev E. V. et al., Journal of Mathematical Sciences 2005 Vol. 128 No. 6 P. 3487-3495

Added: January 27, 2014

Chuprikov P., Nikolenko S. I., Davydow A. et al., IEEE Transactions on Networking 2018 Vol. 26 No. 1 P. 342-355

Modern network elements are increasingly required to deal with heterogeneous traffic. Recent works consider processing policies for buffers that hold packets with different processing requirements (number of processing cycles needed before a packet can be transmitted out) but uniform value, aiming to maximize the throughput, i.e., the number of transmitted packets. Other developments deal with ...

Added: March 14, 2018

Kiselyova N. N., Dudarev V.A., Korzhuev M. A., Inorganic Materials: Applied Research 2016 Vol. 7 No. 1 P. 34-39

A database (DB) on the bandgap of inorganic substances available via the Internet (http://bg.imetdb.ru) was developed for the information service of specialists in the sphere of inorganic chemistry and materials science. The DB is integrated with other information systems on the properties of inorganic substances and materials, which provides the search of a wide range ...

Added: February 23, 2016

Skoptsov K. A., Sheshenin S., Galatenko V. V. et al., International Journal of Applied Mechanics 2016 Vol. 8 No. 2 P. 1650016-01-1650016-18

We present a method for evaluating elastic properties of a composite material produced by molding a resin filled with short elastic fibers. A flow of the filled resin is simulated numerically using a mesh-free method. After that, assuming that spatial distribution and orientation of fibers are not significantly changed during polymerization, effective elastic moduli of ...

Added: May 22, 2016

Malyshev D., Discrete Mathematics 2015 Vol. 338 No. 11 P. 1860-1865

We completely determine the complexity status of the 3-colorability problem for hereditary graph classes defined by two forbidden induced subgraphs with at most five vertices. ...

Added: April 7, 2014

М. : Издательский центр «Российский государственный гуманитарный университет», 2019

Сборник включает 27 докладов международной конференции по компьютерной лингвистике и интеллектуальным технологиям «Диалог 2019», не вошедшие в ежегодник «Компьютерная лингвистика и интеллектуальные технологии», но рекомендованные Программным Комитетом к представлению на конференции. Для специалистов в области теоретической и прикладной лингвистики и интеллектуальных технологий. ...

Added: December 10, 2019

Bliznets Ivan, Cygan M., Komosa P. et al., ACM Transactions on Computation Theory 2018 Vol. 10 No. 2 P. 1-32

The H-free Edge Deletion problem asks, for a given graph G and integer k, whether it is possible to delete at most k edges from G to make it H-free—that is, not containing H as an induced subgraph. The H-free Edge Completion problem is defined similarly, but we add edges instead of deleting them. The study of these two problem families has recently been the subject of intensive studies from the point of ...

Added: October 30, 2018