GRIP · General Reasoning for Imperative Programs
7РП — „Хора“ (Действия „Мария Кюри“)
- Период
- 2015-03-12 → 2017-03-11
- Финансиране от ЕС
- 231 283 €
- Участници
- 1
- Схема
- MC-IEF
Линиите свързват координатора с партньорите.
Накратко на български
Логиката на императивните програми, включително тези с указатели и паралелни процеси, се изследва чрез нови математически модели. Това помага за създаването на по-прости и общи доказателства за коректността на програмния код.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Цел на проекта
It is hard to reason about imperative programs, especially when concurrency and pointers are involved. Such programs are inherently complex, but the reasoning problem is exacerbated by conventional formalisms that demand, and thus encourage, tedious and overly detailed proofs. This project aims to get a GRIP on reasoning by adopting a novel formalisation that holds promise to make proofs simpler and more general. In particular, the goals of GRIP are 1) to equip popular reasoning techniques with simpler semantic foundations that render proofs more tractable, and 2) to accommodate realistic programming languages in a general way. The approach to overcome the complexity of these goals is to separate concerns in a new way: use simple mathematical models and algebraic laws at the core, and build reasoning techniques and languages around it to maximise understanding and reuse.
Оригинален текст от CORDIS (на английски).
Участници
- UNIVERSITY COLLEGE LONDON · LONDONКоординаторнепознат регион
Връзки
Данни: CORDIS, © Европейски съюз