"Muu" projekt IKT29
IKT29 (3.2.1201.13-0029) "Coinduction for semantics, analysis and verification of communicating and concurrent reactive software (1.03.2013−30.11.2015)", Tarmo Uustalu, Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
3.2.1201.13-0029
IKT29
Coinduction for semantics, analysis and verification of communicating and concurrent reactive software
Coinduction for semantics, analysis and verification of communicating and concurrent reactive software
Coinduction for semantics, analysis and verification of communicating and concurrent reactive software
1.03.2013
30.11.2015
Teadus- ja arendusprojekt
Muu
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
AsutusRiikTüüp
SA Archimedes
PerioodSumma
01.03.2013−30.11.2015526 194,00 EUR
526 194,00 EUR
EL struktuuritoetuste meede: 3.2.12 Info- ja kommunikatsioonitehnoloogiate teadus- ja arendustegevuse toetamine

The high-level research goal of the project is to advance the state-of-the-art of mathematical methods and tools for trustworthiness (assurance, monitoring of correctness, safety) of software that reacts to stimuli. Specifically, we will develop frameworks of semantic description, analysis, and verification for programming languages for reactive computing with different communication and concurrency mechanisms. We will apply coinduction and related techniques to represent the relevant computation structures (that typically involve infinite datastructures), program with them, and reason about them. We will formalize the datatypes, algorithms and proofs that we develop in the exploratory dependently typed programming language Agda and, where appropriate, other programming languages and proof assistants, leading to an experimental suite of tools of certified reactive programming. We will conduct this research in an international context with direct involvement in the project of three European universities and active participation of all parties involved in relevant cross-border cooperation networks including the research community behind the TYPES conference series, the Agda implementors (AIM) network, and also the COST ICT action Rich Model Toolkit. We will involve a number of postdocs and PhD students. These research and research capacity building goals match exactly the sub-measure goals of supporting research in promising research directions in ICT, supporting the participation of Estonian R&D institutions in cross-border cooperation networks and supporting actions that foster cooperation with the IT Academy and IKTP implementation programme initiatives.
The high-level research goal of the project is to advance the state-of-the-art of mathematical methods and tools for trustworthiness (assurance, monitoring of correctness, safety) of software that reacts to stimuli. Specifically, we will develop frameworks of semantic description, analysis, and verification for programming languages for reactive computing with different communication and concurrency mechanisms. We will apply coinduction and related techniques to represent the relevant computation structures (that typically involve infinite datastructures), program with them, and reason about them. We will formalize the datatypes, algorithms and proofs that we develop in the exploratory dependently typed programming language Agda and, where appropriate, other programming languages and proof assistants, leading to an experimental suite of tools of certified reactive programming. We will conduct this research in an international context with direct involvement in the project of three European universities and active participation of all parties involved in relevant cross-border cooperation networks including the research community behind the TYPES conference series, the Agda implementors (AIM) network, and also the COST ICT action Rich Model Toolkit. We will involve a number of postdocs and PhD students. These research and research capacity building goals match exactly the sub-measure goals of supporting research in promising research directions in ICT, supporting the participation of Estonian R&D institutions in cross-border cooperation networks and supporting actions that foster cooperation with the IT Academy and IKTP implementation programme initiatives.
KirjeldusProtsent
Alusuuring100,0