Меню
КартаВръзкиТемиБългарияНощта (K-TRIO)Мария Склодовска-КюриЗа ученициЗа учителиМетодологияИзненадай ме
H2020Обмен на изследователи2017–2023

CID · Computing with Infinite Data

„Хоризонт 2020“ — Действия „Мария Склодовска-Кюри“

Период
2017-04-01 → 2023-03-31
Финансиране от ЕС
958 500 €
Участници
21
Схема
MSCA-RISE

Линиите свързват координатора с партньорите. За проекти отпреди 2014 г. CORDIS не винаги дава точни координати. Тези точки са на ниво град или държава.

Накратко на български

Изчисленията с безкрайни обекти, като например десетичните дроби, се анализират от теоретична и практическа гледна точка. Това помага за създаването на софтуер без грешки при закръглянето, което е важно за безопасността на системи като автопилоти или ракети.

Този кратък обзор е генериран от изкуствен интелект

Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.

Резултати накратко

Computing with Infinite Data

The joint research in this programme studies important aspects---both theoretical as well as applied---of computing with infinite objects such as decimal fractions, to mention a key example. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications. More and more applications require the use of computers, but in many situations, computer programs can present inaccuracies due to, for example, rounding errors. However, software inaccuracies can create vulnerabilities which can have unexpected consequences. For example, the first Ariadne 5 launch (a rocket used by the European Space Agency) failed due to that kind of inaccuracies. We develop tools which can help resolve these inaccuracies. The problem is that there is a dissociation between the mathematical theory and its implementation in computer programs. One way out of the problem is to formally prove the correct functioning of engineering applications: The autopilot in an aircraft must work flawlessly, e.g.. Human life depends on the technology being correct at all times. Software is usually tested against a variety of possible scenarios. However, this does not guarantee that the software is completely safe. Vulnerabilities can still exist and can have unintended consequences. Using infinite-precision data helps to develop tools to formally prove that programs function according to their respective requirements, which means that we can be sure that the software works correctly. In another part of the investigation, we would like to understand which problems are inherently difficult or even impossible to solve with the help of computers, and how do they fundamentally differ from easier problems. This knowledge is valuable for software developers, since they do no longer need to spend their time for searching for alternatives in such cases. Work on all of these objectives has been very successful: The logical system for specifying algorithms and extracting algorithms from proofs has been dramatically extended and improved: constructive reasoning is seamlessly integrated with classical logic; an extension for specifications of concurrent processes at a very high level is available and has proven practically useful since it improves efficiency; computational garbage can be completely avoided; computational complexity of computation on infinite data can be controlled through precise estimates of look-ahead. For several important types of differential equations appearing in physics and engineering, the intrinsic complexity of solving them has been determined. On the applied side, existing software packages using infinite-precision data have been further extended and the interplay of the different packages has been facilitated.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз

Цел на проекта

The joint research in this programme will study important aspects—both theoretical as well as applied—of computing with infinite objects. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications. A prime example for infinite data is provided by the real numbers, most commonly conceived as infinite sequences of digits. While most applications in science and engineering substitute the reals with floating point numbers of fixed finite precision and thus have to deal with truncation and rounding errors, the approach in this project is different: exact real numbers are taken as first-class citizens and while any computation can only exploit a finite portion of its input in finite time, increased precision is always available by continuing the computation process.This project aims to bring together the expertise of specialists in mathematics, logic, and computer science to push the frontiers of our theoretical and practical understanding of computing with infinite objects. Three overarching motivations drive the proposed collaboration:Representability. Cardinality considerations tell us that it is not possible to represent arbitrary mathematical objects in a way that is accessible to computation. We will enlist expertise in topology, logic, and set theory, to address the question of which objects are representable and how they can be represented most efficiently.Constructivity. Working in a constructive mathematical universe can greatly enhance our understanding of the link between computation and mathematical structure. Not only informs us which are the objects of relevance, it also allows us to devise always correct algorithms from proofs.Efficient implementation. We also aim to make progress on concrete implementations. Theoretical insights from elsewhere will be tested in actual computer systems; obstacles encountered in the latter will inform the direction of mathematical investigation.

Оригинален текст от CORDIS (на английски).

Участници

Връзки

Данни: CORDIS, © Европейски съюз