Tugevalt tagatud tarkvara laboratoorium

Projekt uurib uusi sõltuvate tüüpidega tüübisüsteme, mis on sobilikud programmeerimiskeelte semantikate arendamiseks ja formaliseerimiseks tõestusassistentide abil. Eriline rõhk on keeltel, mis toetavad konkurentsust ja mittedetermiminismi, nt oleku-siirdesüsteemid ja protsessiarvutused. Populaarsed tüübiteoreetilised tõestusassistendid nagu Agda ja Coq ei sobi niisuguste keelte denotatsioonsemantika esitamiseks, kuna nende tüübisüsteemid ei ole piisavalt väljendusvõimsad. Me vastame sellele väljakutsele sel moel, et toome kaasaegsetesse tüübiteoreetilistesse raamistutesse nagu homotoopiline tüübiteooria sisse uue klassi koinduktiivseid tüüpe, mis esitavad saavutatavate funktorite terminaalseid koalgebraid. Denotatsioonsemantikas läheb protsesside mittedeteministliku ja interageeruva käitumise esitamiseks vaja tüüpe just sellest klassist. Loodavad väljendusvõimsamad tüübisüsteemid lubavad konkurentsuse ja mittedeterminismiga keelte formaalset semantikat adekvaatselt kodeerida.

LaineTeisik projekti eesmärk on edasi arendada digitaalset teisikut, et hinnata Läänemere lainetuse energia jaotust (spekter) satelliit tehisavaradari (SAR) andmete põhjal. Varasemalt välja töötatud meetodid SAR andmetele pole piisavalt edukad suletud veekogude puhul, kus domineerivaks on lühikesed ja järsud tuulelained. On ilmselge, et kogu Läänemere pindala ei saa katta lainepoidega, et lainetust mõõta. SAR andmete kasutamine võimaldab meil efektiivselt hinnata lainespektrit üle terve Läänemere jättes vahele suured lainemõõtjate veeskamise ja opereerimise kulud. Eesmärgi saavutamiseks kasutab meeskond oma teadmisi süvaõppe tehnikate rakendamisel, et hinnata SAR-piltide põhjal laine spektrit ehk laine energia jaotumist sageduste kaupa. Keskkonnakaitse ja navigatsioon merel (nt tuuleparkide ehitamise ja hooldamise jaoks) on kaks kõige peamisemat rakendusvaldkonda. Kasvav huvi selliste probleemide vastu ilmneb ka olukorrateadlikkuse süsteemide valdkonnas.

The central research focus of the technology and economics of trust in software theme will be certified software. Topics of research include: • methods and tools for certification of software; program analysis, transformation, generation; in particular for big data, cloud and IoT; • static analysis (model checkers, theorem provers), verification, systematic testing; • contract languages, languages with powerful type systems (refinement types, dependent types); domain-specific languages; • program synthesis and program learning, program understanding; • repositories of certified software, evolution of certified software; • trust in closed-source software, gradual trust-building; • trading trust, pricing of trust, game theory of trust.