• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
Of all publications in the section: 98
Sort:
by name
by year
Article
Grigorev S., Bozhko S., Хатбуллина Л. Р. Lecture Notes in Computer Science. 2019. Vol. 11541. P. 264-281.

Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verifica- tion, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theo- rem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.

Added: Aug 20, 2019
Article
Savelieva A., Khovratovich D., Rechberger C. Lecture Notes in Computer Science. 2012. Vol. 7549 LNCS. P. 244-263.

We present a new concept of biclique as a tool for preimage attacks, which employs many powerful techniques from differential cryptanalysis of block ciphers and hash functions. The new tool has proved to be widely applicable by inspiring many authors to publish new results of the full versions of AES, KASUMI, IDEA, and Square. In this paper, we show how our concept leads to the first cryptanalysis of the round-reduced Skein hash function, and describe an attack on the SHA-2 hash function with more rounds than before.

Added: Feb 7, 2013
Article
Kurmukov A., Ananyeva M., Dodonova Y. et al. Lecture Notes in Computer Science. 2017. P. 3-11.

Human anatomical brain networks derived from the analysis of neuroimaging data are known to demonstrate modular organization. Modules, or communities, of cortical brain regions capture information about the structure of connections in the entire network. Hence, anatomical changes in network connectivity (e.g., caused by a certain disease) should translate into changes in the community structure of brain regions. This means that essential structural differences between phenotypes (e.g., healthy and diseased) should be reflected in how brain networks cluster into communities. To test this hypothesis, we propose a pipeline to classify brain networks based on their underlying community structure. We consider network partitionings into both non-overlapping and overlapping communities and introduce a distance between connectomes based on whether or not they cluster into modules similarly. We next construct a classifier that uses partitioning-based kernels to predict a phenotype from brain networks. We demonstrate the performance of the proposed approach in a task of classifying structural connectomes of healthy subjects and those with mild cognitive impairment and Alzheimer’s disease.

Added: May 30, 2021
Article
Андрианов П. С., Мутилин В. С., Khoroshilov A. V. Lecture Notes in Computer Science. 2021. Vol. 12652. P. 423-427.

Our submission to SV-COMP’21 is based on the software verification framework CPAchecker and implements the extension to the thread-modular approach. It considers every thread separately, but in a special environment which models thread interactions. The environment is expressed by projections of normal transitions in each thread. A projection contains a description of possible effects over shared data and synchronization primitives, as well as conditions of its application. Adjusting the precision of the projections, one can find a balance between the speed and the precision of the whole analysis.

Implementation on the top of the CPAchecker framework allows combining our approach with existing algorithms and analyses. Evaluation on the sv-benchmarks confirms the scalability and soundness of the approach.

Added: Jun 22, 2021
Article
Kamkin A., Khoroshilov A. V., Коцыняк А. М. et al. Lecture Notes in Computer Science. 2020. Vol. 12165. P. 43-58.

There is a high demand in practical methods and tools to ensure total correctness of critical software components. A usual assumption is that the machine code (or binary code) generated by a compiler follows the semantics of the programming language. Unfortunately, modern compilers such as GCC and LLVM are too complex to be thoroughly verified, and bugs in the generated code are not uncommon. As an alternative approach, we suggest proving that the generated machine code still satisfies the functional properties expressed at the source code level. The suggested approach takes an ACSL-annotated C function along with its binary code and checks that the binary code meets the ACSL annotations. The main steps are as follows: (1) disassembling the machine code and extracting its semantics; (2) adapting the annotations to the machine level and generating the verification conditions. The implementation utilizes MicroTESK, Frama-C, Why3, and other tools. To illustrate the solution, we use the RISC-V microprocessor architecture; however, the approach is relatively independent of the target platform as it is based on formal specifications of the instruction set. It is worth noting that the presented method can be exploited as a test oracle for compiler testing.

Added: Jun 22, 2021
Article
Nascimento S., Mirkin B. Lecture Notes in Computer Science. 2011. Vol. 6743. P. 273-277.
Added: Feb 1, 2012
Article
Grishunin S., Suloeva S. Lecture Notes in Computer Science. 2016. No. 9870. P. 752-765.

We developed the project risk rating (PRR) for telecommunication companies. It provides qualitative risk scores assessment of capital expenditures (capex) projects to rank them by severity of exposures, to check their fit into the company’s risk profile and, ultimately, to combine projects into the efficient project portfolio with the lowest risk given return. We discussed the definition, functions and advantages of investment controlling and presented the reference model of its main subsystem – project portfolio controlling responsible for building the efficient capex project portfolio. Then, we developed the model of PRR; worked out the example of PRR’s scorecard and discussed the advantages of the PRR over the existing risk assessment tools in project portfolio management.

Added: Oct 20, 2019
Article
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 e ectively 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: Sep 30, 2015
Article
Maxim Babenko. Lecture Notes in Computer Science. 2013. Vol. 7741. P. 146-156.

Let G = (V,E) be a digraph with disjoint sets of sources S ⊂ V and sinks T ⊂ V endowed with an S–T flow f : E → Z+. It is a well-known fact that f decomposes into a sum_st(fst) of s–t flows fst between all pairs of sources s ∈ S and sinks t ∈ T . In the usual RAM model, such a decomposition can be found in O(E log V 2 E ) time. The present paper concerns the complexity of this problem in the external memory model (introduced by Aggarwal and Vitter). The internal memory algorithm involves random memory access and thus becomes inefficient. We propose two novel methods. The first one requires O(Sort(E) log V 2 E ) I/Os and the second one takes O(Sort(E) log U) expected I/Os (where U denotes the maximum value of f).

Added: Nov 13, 2013
Article
Magizov R. A. Lecture Notes in Computer Science. 2011. Vol. 6743. P. 258-264.
Added: Mar 6, 2012
Article
Makarenko A., Goldengorin B. I., Krushinsky D. Lecture Notes in Computer Science. 2008. Vol. 5191. P. 77-82.
Added: Jul 31, 2012
Article
Pardalos P. M., Shylo O., Korenkevych D. Lecture Notes in Computer Science. 2012. Vol. 7492 LNCS. No. 2. P. 277-286.
Global Equilibrium Search (GES) is a meta-heuristic framework that shares similar ideas with the simulated annealing method. GES accumulates a compact set of information about the search space to generate promising initial solutions for the techniques that require a starting solution, such as the simple local search method. GES has been successful for many classic discrete optimization problems: the unconstrained quadratic programming problem, the maximum satisfiability problem, the max-cut problem, the multidimensional knapsack problem and the job-shop scheduling problem. GES provides state-of-the-art performance on all of these domains when compared to the current best known algorithms from the literature. GES algorithm can be naturally extended for parallel computing as it performs search simultaneously in distinct areas of the solution space. In this talk, we provide an overview of Global Equilibrium Search and discuss some successful applications.
Added: Feb 7, 2013
Article
Muravyov D. Lecture Notes in Computer Science. 2019. Vol. 11551. P. 237-243.

Despite the fact that working with imaginaries is already widely acknowledged in Internet studies their use in Internet policy studies still remains limited. In this paper, I approach studying Internet governance from the perspective of “sociotechnical imaginaries”. I argue that this concept can prove to be especially useful in studying authoritarian policy-settings and elucidate the relationship between stakeholders in the field of Internet governance.

Added: Nov 16, 2020
Article
Nascimento S., Fenner T., Felizardo R. et al. Lecture Notes in Computer Science. 2011. Vol. 6744. P. 3-12.
Added: Feb 1, 2012
Article
Stegailov V., Orekhov N., Smirnov G. Lecture Notes in Computer Science. 2015. Vol. 9251. P. 469-473.

Development of new HPC architectures proceeds faster than the corresponding adjustment of the algorithms for such fundamental mathematical models as quantum and classical molecular dynamics. There is the need for clear guiding criteria for the computational efficiency of a particular model on a particular hardware. LINPACK benchmark alone can no longer serve this role. In this work we consider a practical metric of the time-to-solution versus the computational peak performance of a given hardware system. In this metric we compare different hardware for the CP2K and LAMMPS software packages widely used for atomistic modeling. The metric considered can serve as a universal unambiguous scale that ranges different types of supercomputers.

Added: Jul 5, 2016
Article
Kuznetsov S., Poelman J., Elzinga P. et al. Lecture Notes in Computer Science. 2012. Vol. 7377 LNAI. P. 528-272.
In this paper we introduce a novel human-centered data mining software system which was designed to gain intelligence from unstructured textual data. The architecture takes its roots in several case studies which were a collaboration between the Amsterdam-Amstelland Police, GasthuisZusters Antwerpen (GZA) hospitals and KU Leuven. It is currently being implemented by bachelor and master students of Moscow Higher School of Economics. At the core of the system are concept lattices which can be used to interactively explore the data. They are combined with several other complementary statistical data analysis techniques such as Emergent Self Organizing Maps and Hidden Markov Models.
Added: Feb 7, 2013
Article
Vyalyi M., Gimadeev R. Lecture Notes in Computer Science. 2010. Vol. 6072. P. 144-155.
Added: Oct 18, 2014
Article
Nasonova A., Nasonov A., Krylov A. et al. Lecture Notes in Computer Science. 2014. Vol. 8815. P. 159-166.

The paper focuses on solving the problem of hair removal in dermatology applications. The proposed hair removal algorithm is based on Gabor filtering and PDE-based image reconstruction. It also includes the edge sharpening stage using a new warping algorithm. The idea of warping is to move pixels from the neighborhood of the blurred edge closer to the edge. The proposed technique preserves the overall luminosity and textures of the image, while making the edges sharper and less noisy.

Added: Oct 20, 2015
Article
Goldengorin B. I., Sierksma G., Ghosh D. Lecture Notes in Computer Science. 2001. Vol. 2141. P. 106-117.
Added: Jul 31, 2012
Article
Richter D., Goldengorin B. I., Jager G. et al. Lecture Notes in Computer Science. 2007. Vol. 4851. P. 99-111.
Added: Jul 31, 2012
Article
Goldengorin B. I., Richter D. Lecture Notes in Computer Science. 2007. Vol. 4852. P. 99-111.
Added: Oct 13, 2010