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, hakatuseks konkreetselt suurte konkurentsete süsteemide automaatsest verifitseerimisest mudelikontrolli teel. Jätkuteemaks võiks saada teoreemitõestamise kasutamine verifitseerimises vms.
Al 10.2.2000 toimub seminar neljapäeviti kl 11 (täpselt) Küberneetika Instituudi ruumis B216 (end B221), kestusega umbes 1.5 tundi. (Varem oli algusajaks kl 16. Kõige esimene kokkusaamine oli 11.11.1999.) Iga huviline on teretulnud kaasa lööma.
(Vt esimest kutset.)
| Kuupäev | Teema | Ettekandja |
|---|---|---|
| 11.11. | Mis mudelikontroll on ja miks sel teel saab ja tasub verifitseerida | Tarmo U |
| 18.11. | Lineaaraja temporaalloogika PLTL | Tarmo U |
| 25.11. | PLTLi mudelikontroll | Marko K |
| 2.12. | PLTLi mudelikontroll (jätk), SPINi demo [ruumis B317, end B321] | Marko K + Tarmo U |
| 9.12. | Mis on BDDd (binaarsed otsustusdiagrammid) | Juhan E |
| 16.12. | BDDdest veel + nende tululikkusest mudelikontrollis ("sümboolne" mudelikontroll) | Juhan E + Tarmo U |
| 23.12. | Mis on BEDd (Boole'i avaldiste diagrammid) | Marko K |
| 6.1. | Lamport sellest, kuidas kirjutada tõestusi ja valemeid | Juhan E |
| 13.1. | Struktuursest kalkuleerivast tõestamisest | Tarmo U |
| 20.1. | CTL, Hennessy-Milneri loogika, PDL | Tarmo U |
| 27.1. | Kozeni müü-arvutus | Tarmo U |
| 3.2. | CTLi mudelikontroll | Marko K |
| 10.2. kl 12 |
(Reaal)ajaga automaadid ja nende kirjeldamine UPPAALis [ruumis B317, end B321] | Marko K + Juhan E |
| 17.2. | (Reaal)ajaga loogikad ja nende mudelikontroll | Tarmo U + Jüri V |
| 27.2.-2.3. | EATTK'00 | |
| 9.3. kl 10 |
Teoreemitõestamise strateegiatest ja nende realiseerimisest | Tanel Tammet |
| 16.3. | Mis on CDDd (kellavahediagrammid) | Juhan E |
| 23.3. kl 10 |
Teoreemitõestamise strateegiatest ja nende realiseerimisest (jätk) | Tanel Tammet |
| 30.3. kl 10 |
Teoreemitõestamise strateegiatest ja nende realiseerimisest (jätk) | Tanel Tammet |
| 6.4. | Prolog, default-loogika, tsirkumskribeerimine ja müü-arvutus | Tarmo U |
| 13.4. | Modulaarne mudelikontroll | Juhan E |
| 20.4. kl 10 |
Teoreemitõestamise strateegiatest ja nende realiseerimisest (jätk) | Tanel Tammet |
| 27.4. kl 10 |
Teoreemitõestamise strateegiatest ja nende realiseerimisest (jätk) | Tanel Tammet |
| 4.5. kl 10 |
Kõrgemat järku loogikate teoreemitõestajad (PVS, ISABELLE) | Marko K |
| 11.5. | Kompositsiooniline projekteerimine | Jüri V |
| 25.5. | Kokkuvõttev seminar | Marko K jt |
Juhan Ernits