The transformation and verification of the bus_sort_breadthfirst program, which belongs to the Linux OS kernel and implements sorting of devices are described. The C program is transformed into the cP language performing macros unfolding, structure changes, and elimination of pointers. Transformed program is translated into the WhyML functional language. For the received program, a specification is constructed. Deductive verification is carried out in the tool Why3.

The article presents a database model based on a sequence of objects. The issues of serialization/deserialization of objects, index constructions, structure and methods of the universal sequence and universal index, implementation of the complete editing basis through the use of the primary key, timestamp and "empty" value are considered.

It is shown that a specification in the Event-B language can be represented by an automata-based program as a non-deterministic composition of simple conditional statements, which corresponds to a narrow subclass of automata-based programs. A specification in Event-B is monolithic. To build a specification, there are no other means of composition, except for a refinement that implements an extension of a previously built specification. Comparison of automata-based engineering method and Event-B modeling method is carried out on two example tasks. Previous solutions to the bridge traffic control problem in the Event-B system are complicated. A simpler solution with deductive verification in the Rodin tool is proposed. The effectiveness of the Event-B verification methods is confirmed by finding three non-trivial errors in our solution.

The article presents the results of experiments on the conjunctive decomposition of various representations of Boolean functions (ZDD, BDD, OKFDD, AIG) by methods that are derived by specializing the general decomposition algorithm. Test sets are random Boolean functions with various parameters, as well as a set of well-known benchmarks used to test algorithms for optimizing logic circuits. The comparison involves sequential and multi-threaded implementation of the algorithm.