Tugevalt tagatud tarkvara laboratoorium

Nimetus
High-assurance software laboratory
Head of the research group
Overview
Rühm uurib tugevalt tagatud tarkvara arendamise teooriaid, meetodeid ja tööriistu, spetsialiseerudes nii tõestustele (sertifitseeritud tarkvara) kui ka testimisele. Viimastel aastatel on eraldi uurimisvaldkonnaks kujunenud rakenduslik masinõpe.
The group conducts research into theories,methods and tools for developing high-assurancesoftware, specializing on both proofs (certifiedsoftware) and testing.
Keyword
funktsionaalne ja sõltuvalt tüübitud programmeerimine
functional and dependently-typed programming
tarkvara verifitseerimine ja testimine
software verification and testing
formaliseeritud programmeerimisteooria
formalized programming theory
Important results
2024. a uurimistulemused:• Töötati välja relatiivsete monaadide formaalne teooria (N. Arkor, D. McDermott) ja konkurentsetemonaadide teooria (E. Rivas, T. Uustalu); nood on monaadide spetsialisatsioon, misaksiomatiseerivad arvutuste rööpkompositsiooni samadel alustel jadakompositsiooniga• Oma magistritöös arendas T. Annus koos juhendaja P. Joramiga välja tüübipõhise termiotsimisealgoritmi programmeerimiskeelele Rust; see funktsionaalsus kaasati Rusti standardtoe hulka.• Käekirja analüüsi põhjal arendati välja Parkinsoni tõve diagnoosija (S. Nõmm, A. Toomela, K.Medijainen).• Hinnati asjade interneti botnettide avastamise tehisaru seletavust (R. Kalakoti, S. Nõmm, H. Bahsi)
A dataset for detection of Android malware wascollected and curated that covers the full historyof the operating system.A construction was given for a digital signaturescheme that makes it possible to use the samekey pair multiple times based on timestamping.Focused sequent calculi were identified for partially normal skew monoidal, skew prounitalclosed and skew symmetric monoidal closedcategories.
Firsov, D.; Unruh, D. (2023). Zero-knowledge in Easycrypt. 2023 IEEE 36th Computer Security Foundations Symposium (CSF): Dubrovnik, Croatia, July 9-13, 2023. IEEE, 1−16. DOI: 10.1109/CSF57540.2023.00015
Haselwarter, P. G.; Rivas, E.; Van Muylder, A.; Winterhalter, T.; Abate, C.; Sidorenco, N.; Hriţcu, C.; Maillard, K.; Spitters, B. (2023). SSProve: a foundational framework for modular cryptographic proofs in Coq. ACM Transactions on Programming Languages and Systems, 45 (3), art. no. 15 −61 pp. DOI: 10.1145/3594735
Wang, X.; Huang, J.; Chatzakou, M.; Nõmm, S.; Valla, E.; Medijainen, K.; Taba, P.; Toomela, A.; Ruzhansky, M. (2023). Comparison of one- two- and three-dimensional CNN models for drawing-testbased diagnostics of the Parkinson's disease. Biomedical Signal Processing and Control, 87 (B), Art. no. 105436−8 pp. DOI: 10.1016/j.bspc.2023.105436