Naslov diplomskega dela: Verjetnostna separacijska logika

Povzetek:

To delo obravnava programsko verjetnostno separacijsko logiko in jo razvije
z novo semantiko programskega jezika, logičnih formul ter novim pravilom
okvirja. Sintaksi programskega jezika so dodani tipi, medtem ko je za
semantiko programskega jezika uporabljena monadna denotacijska semantika.
Zanjo je potrebna uporaba teorije domen, ki je v tem delu tudi na
kratko predstavljena. Semantika jezika je razširjena tudi z nedefiniranimi
spremenljivkami. Logika pa je razširjena s tretjo resničnostno vrednostjo —
nedefinirano. Pravilo okvirja se bistveno poenostavi z odstranitvijo večine
stranskih pogojev. Dokazana je pravilnost poenostavljene različice pravila
okvirja. Prav tako je prikazana uporaba logike na primerih kriptografskih
protokolov.

Mentor: prof. dr. Alexander Keith Simpson

Komisija za zagovor:

prof. dr. Gašper Fijavž (predsednik),

prof. dr. Alexander Keith Simpson (mentor),

izr. prof. dr. Matija Pretnar (član).

Prostor: predavalnica 3.07 (stavba Matematika, Jadranska 21, 3. nadstropje), Fakulteta za matematiko in fiziko