Formaalmeetodite mitteformaalseminar on Küberneetika Instituudi seminar, mille eesmärgiks on sundimatus õhkkonnas mõõdukas tempos tutvuda mitmesuguste kontseptsioonide, tehnikate ja töövahenditega formaalmeetodite alalt. Konkreetsemalt tahaks tutvust teha protsessialgrebratega ja täpsustusega (refinement). Selleaastane seminar on jätkuks eelmisel talvel ning kevadel toimunud Tarmo Uustalu algatatud seminarile. See ei tähenda aga sugugi, et osavõtjate hulgas ei võiks olla neid, kes kevadel seminari ei kuulanud.
Seminarid toimuvad esmaspäeviti kl 15.45 Küberneetika Instituudi ruumis B216. Seminari kestus on umbes 1.5 tundi.
Iga huviline on teretulnud kaasa lööma.
| Kuupäev | Teema | Ettekandja |
|---|---|---|
| N 12.10. kl 14 |
Kitsendustega programmeerimine (constraint programming) tuginedes Thom Frühwirthi loengule | Juhan E |
| 16.10. | Veakindel disain kasutades spetsifitseerimismetoodikat OUN | Jüri Vain |
| 23.10. | Veakindel disain kasutades spetsifitseerimismetoodikat OUN - näide | Jüri Vain |
| 06.11. | Verifitseerimine abstraktsioonide abiga Lõpmatu olekuruumiga süsteemi verifitseerimisel abstraheerikse see vastavalt testitavale omadusele lõplikumõõtmeliseks ja kasutakse siis mudelkontrolli. Nii õnnestub asendada deduktiivset tõestust/verifitseerimist. On võimalik näidata, et vähemalt LTLi puhul on see meetod võrdväärne deduktiivse tõestusega - abstraheerimine esindab tõestuse intelligentset osa (lemmade leiutamine) ja mudelkontroll mehaanilist osa. Materjalid: Amir Pnueli ettekande abstract ja slaidid. Artikkel "Modularization and Abstraction: The Keys to Practical Formal Verification". Vahend, mis kasutab sellist abstraheerimise tehnikat automaatselt. |
Marko K |
| 13.11. | Verifitseerimine abstraktsioonide abiga (jätk) | Marko K |
| 20.11. | Stepwise development of dependable systems | Elena Troubitsyna (Åbo Akademi) |
| 27.11. | Kitsendustega programmeerimine (constraint programming) tuginedes Thom Frühwirthi loengule (jätk) | Juhan E |
| 04.12. kl 16 |
Kiire ülevaade erinevatest programmeerimisparadigmadest: dünaamiline planeerimine, ahne algoritm, backtracking, branch&bound | Marko K |
| 11.12. | Tõestust sisaldav programmikood tuginedes Peter Lee loengule | Juhan E |
| 18.12. | Tüübitud assembler | Varmo Vene
(Tartu Ülikool) |
| 5.2. | Viitadest temporaalloogikates ja milleks need kasulikud võivad olla, Val Goranko järgi | Tarmo U |
| 19.2. | Programmide automaatne süntees Java keeles | Vahur Kotkas |
| P-R 4.-9.3. |
EWSCS '01 | |
| 19.3. | Järjestikprogrammide verifitseerimine | Jüri Vain |
Ettepanekud seminari teemade ja nende esitamisaegade osas palun saata e-postiga.
Juhan Ernits