• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Using Parallel Computations in Deductive Synthesis of Functional Programs
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
May 20, 2026
HSE University Opens First Representative Office of Satellite Laboratory in Brazil
HSE University-St Petersburg opened a representative office of the Satellite Laboratory on Social Entrepreneurship at the University of Campinas in Brazil. The platform is going to unite research and educational projects in the spheres of sustainable development, communications and social innovations.
May 18, 2026
The 'Second Shift' Is Not Why Women Avoid News
Women are more likely than men to avoid political and economic news, but the reasons for this behaviour are linked less to structural inequality or family-related stress than to personal attitudes and the emotional perception of news content. This conclusion was reached by HSE researchers after analysing data from a large-scale survey of more than 10,000 residents across 61 regions of Russia. The study findings have been published in Woman in Russian Society.
May 15, 2026
Preserving Rationality in a Period of Turbulence
The HSE International Laboratory for Logic, Linguistics and Formal Philosophy studies logic and rationality in a transformed world characterised by a diversity of logical systems and rational agents. The laboratory supports and develops academic ties with Russian and international partners. The HSE News Service spoke with the head of the laboratory, Prof. Elena Dragalina-Chernaya, about its work.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

Using Parallel Computations in Deductive Synthesis of Functional Programs

P. 67–72.
Korukhova Y., Fastovets N.
The paper deals with deductive synthesis of functional programs. This approach means that we take as our input data a specification of program, it is treated as a mathematical existence theorem and while proving it constructively we derive a program. If the derivation is successful the resulted program does not require verification: it is proven that it corresponds to all the specified requirements. Despite the fact that there are several theoretical methods that gives the rules for proof construction and program derivation they usually do not work in automated synthesis systems because of exponentially growing search space of possible proof attempts. We are trying to solve this problem using recent changes in computer architecture: the possibility of parallel execution of proofs or their steps is discussed. The proposed ideas were implemented in the system Icarus and used for the synthesis of some examples.   
Language: English
Keywords: parallel computingdeductive program synthesis

In book

Scientific Computing: Proceedings of the International Eugene Lawler PhD School
Waterford: Waterford Institute of Technology, 2014.
Similar publications
Performance Analysis of Computational Devices in Quantum Chemistry Tasks
Nedomolkin I., Konikov M., Fedorov I. et al., , in: Parallel Computational Technologies, 19th International Conference, PCT 2025, Moscow, Russia, April 8–10, 2025, Revised Selected PapersVol. 2891.: Springer, 2026. P. 513–531.
Modern supercomputer systems play a crucial role in scientific and engineering research. To ensure their effectiveness, these fields require reliable methods for evaluating supercomputer performance. Although benchmarking is a fundamental tool, current ranking systems often inadequately represent real-world performance in high-performance computing (HPC) applications. As a result, employing actual scientific software packages provides a more ...
Added: May 19, 2026
Hardware-Software Complex for Network-on-Chip Prototyping Using Multiple FPGAs
Mikhail Y. Romashikhin, Aleksandr Y. Romanov, IEEE Access 2026 Vol. 14 P. 7921–7931
This paper presents a hardware-software multi-FPGA complex designed for hardware prototyping of networks-on-chip (NoCs). The rationale for the use of multiple FPGAs for NoC prototyping is given. The architecture of the complex and its components–the software part generating top-level files and configuration files describing the NoC for several FPGAs, hardware part consisting of interfacing switches ...
Added: January 22, 2026
GEMM Algorithm for Multi-GPU Platforms with Regular Uneven Data Transfer Links
Choi Y. R., Malkovsky S., Stegailov V., , in: 11th Russian Supercomputing Days, RuSCDays 2025, Moscow, Russia, September 29–30, 2025, Revised Selected Papers.: Springer, 2026. Ch. 3 P. 32–47.
Multi-GPU servers often exhibit uneven characteristics. For instance, the data transfer bandwidth between four NVIDIA V100 GPUs can vary due to the NVLink connecting these devices to a specific CPU in servers with IBM POWER 9 processors, which means that the communication bandwidth between other devices is comparably slower. To address this issue, the Multi-GPU ...
Added: January 3, 2026
«Cтройка» – компьютерная игра для знакомства с параллельным программированием
Воронова К. Д., Plaksin M. A., В кн.: Актуальные проблемы математики, механики и информатики 2022: Сборник статей по материалам студенческой конференции (г. Пермь, ПГНИУ, 25 мая – 10 июня 2022 г.).: Пермь: ПГНИУ, 2022. С. 25–29.
The rapid development of parallel computing technologies makes it urgent to include propaedeutics of parallel computing in the school computer science course. Since this topic is not yet included in the school curriculum, it can be done through extracurricular activities, in particular, through Internet contests. Since 2013, parallel computing tasks have become a compulsory part ...
Added: February 29, 2024
Methods for Changing Parallelism in the Process of High-Level VLSI Synthesis
Ryzhenko I. N., Nepomnyaschy O. V., A. I. Legalov et al., Automatic Control and Computer Sciences 2023 Vol. 57 No. 7 P. 696–705
In this paper, methods for increasing the efficiency of VLSI development based on the method of architecture-independent design are proposed. The route of high-level VLSI synthesis is considered. The principle of constructing a VLSI hardware model based on the functional-flow programming paradigm is stated. The results of the development of methods and algorithms for the ...
Added: February 27, 2024
GPU-Accelerated Matrix Exponent for Solving 1D Time-Dependent Schrödinger Equation
Choi Y. R., Stegailov V., , in: Supercomputing: 9th Russian Supercomputing Days, RuSCDays 2023, Moscow, Russia, September 25–26, 2023, Revised Selected Papers, Part I.: Springer, 2023. P. 100–113.
Non-adiabatic electron-ion quantum dynamics is still an area of many unresolved problems even for such simple systems as the H2+ molecular ion. Mathematical modelling based on time-dependent Schrödinger equation (TDSE) is an important method that can provide better understanding of these phenomena. In this work, we present TDSE solution for 1D TDSE that describes non-adiabatic electron-ion ...
Added: January 26, 2024
Multi-GPU GEMM Algorithm Performance Analysis for Nvidia and AMD GPUs Connected by NVLink and PCIe
Choi Y. R., Stegailov V., , in: 22nd International Conference, MMST 2022, Nizhny Novgorod, Russia, November 14–17, 2022, Revised Selected Papers.: Springer, 2022. Ch. 23 P. 281–292.
Modern types of multi-GPU servers combine up to 8 A100 GPUs connected by NVLink 3.0 links through NVSwitch. This connectivity provides unprecedented capabilities for multi-GPU algorithms. In this work, we analyze the performance of matrix-matrix multiplication algorithm developed by us previously. Tuning principles and limits for maximum performance are discussed. Algorithm performance for much more ...
Added: December 26, 2022
ЗНАКОМСТВО С ПАРАЛЛЕЛЬНЫМИ ВЫЧИСЛЕНИЯМИ В РАМКАХ ДИСТАНЦИОННОГО КОНКУРСА «ТРИЗФОРМАШКА-2022»
Воронова К. Д., Plaksin M. A., В кн.: Дистанционное обучение – образовательная среда XXI века : материалы XII Междунар. науч.-метод. конф. (Республика Беларусь, Минск, 26 мая 2022 года).: Мн.: БГУИР, 2022. С. 163–163.
It is proposed to introduce schoolchildren and students to the basics of parallel computing using the distance competition "TRIZformashka". For the competition "TRIZformashka-2022" the computer game "Builder" was specially developed for teaching how to build parallel algorithms. A description of the game and a download link are given. ...
Added: October 31, 2022
Supercomputing: 7th Russian Supercomputing Days, RuSCDays 2021, Moscow, Russia, September 27–28, 2021, Revised Selected Papers
Springer, 2021.
Added: October 19, 2022
Tuning of a Matrix-Matrix Multiplication Algorithm for Several GPUs Connected by Fast Communication Links
Choi Y. R., Nikolskiy V., Stegailov V., , in: Parallel Computational Technologies: 16th International Conference, PCT 2022, Dubna, Russia, March 29–31, 2022, Revised Selected Papers.: Springer, 2022. Ch. 12 P. 158–171.
Added: August 11, 2022
Методы преобразования параллелизма в процессе высокоуровневого синтеза СБИС
Рыженко И. Н., Непомнящий О. В., Легалов А. И. et al., Моделирование и анализ информационных систем 2022 Т. 29 № 1 С. 60–72
In this paper methods for increasing the efficiency of VLSI development based on the method of architecture-independent design are proposed. The route of high-level VLSI synthesis is considered. The principle of constructing a VLSI hardware model based on the functional-flow programming paradigm is stated. The results of the development of methods and algorithms for transformation functional-parallel ...
Added: March 18, 2022
Supercomputing. RuSCDays 2020. Communications in Computer and Information Science
Switzerland: Springer, 2020.
This book constitutes the refereed post-conference proceedings of the 6th Russian Supercomputing Days, RuSCDays 2020, held in Moscow, Russia, in September 2020.* The 51 revised full and 4 revised short papers presented were carefully reviewed and selected from 106 submissions. The papers are organized in the following topical sections: parallel algorithms; supercomputer simulation; HPC, BigData, AI: ...
Added: December 10, 2020
Matrix-Matrix Multiplication Using Multiple GPUs Connected by Nvlink
Choi Y. R., Nikolskiy V., Stegailov V., , in: 2020 Global Smart Industry Conference (GloSIC).: IEEE, 2020. P. 354–361.
Added: December 3, 2020
Метод архитектурно-независимого высокоуровневого синтеза СБИС
Легалов А. И., Непомнящий О. В., Рыженко И. Н., Известия ЮФУ. Технические науки 2018 Т. 202 № 8 С. 38–47
The problem of high-level design of complex functional circuits and systems intended for implementation in the form of VLSI is considered. The basic shortcomings of existing approaches are revealed and a conceptually new method of project synthesis is proposed. The method is based on the functional-streaming paradigm of parallel computing, it allows for implementation of ...
Added: October 29, 2020
Параллельные вычислительные технологии (ПаВТ'2020)
Chelyabinsk: ., 2020.
Added: October 23, 2020
PPAM 2019: Parallel Processing and Applied Mathematics. Lecture Notes in Computer Science
Springer, 2020.
This volume comprises the proceedings of the 13th International Conference on Parallel Processing and Applied Mathematics (PPAM 2019), which was held inBiałystok, Poland, September 8–11, 2019. It was organized by the Department of Computer and Information Science of the Częstochowa University of Technology together with Białystok University of Technology, under the patronage of the Committee ...
Added: October 14, 2020
Parallel Computing: Technology Trends
IOS Press, 2020.
The year 2019 marked four decades of cluster computing, a history that began in 1979 when the first cluster systems using Components Off The Shelf (COTS) became operational. This achievement resulted in a rapidly growing interest in affordable parallel computing for solving compute intensive and large scale problems. It also directly lead to the founding ...
Added: March 27, 2020
Parallel Computing Technologies. PaCT 2019. Lecture Notes in Computer Science, vol 11657
Springer, 2019.
Added: October 19, 2019
Parallel Computational Technologies. 12th International Conference, PCT 2018, Rostov-on-Don, Russia, April 2–6, 2018, Revised Selected Papers
Cham: Springer, 2018.
This book constitutes the refereed proceedings of the 12th International Conference on Parallel Computational Technologies, PCT 2018, held in Rostov-on-Don, Russia, in April 2018. The 24 revised full papers presented were carefully reviewed and selected from 167 submissions. The papers are organized in topical sections on high performance architectures, tools and technologies; parallel numerical algorithms; supercomputer simulation. ...
Added: March 11, 2019
Пропедевтика параллельных вычислений в школьной информатике: компьютерная игра «Пожарные танки»
Plaksin M. A., Щелкунов А. А., Современные информационные технологии и ИТ-образование 2018 Т. 14 № 4 С. 1000–1011
The article contains the  methodological materials for inclusion of the topic “Parallel Computing” in the school informatics. The computer games “Tank crew”, “Swarm of robots”, “Firefighting vehicles” are considered. The goal of the first game is to program joint actions of tank crew members. The plot of the second game is the putting on foot ...
Added: January 7, 2019
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit