20.500.12556/RUL-170333 Verjetnostna separacijska logika Probabilistic Separation Logic 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. This work addresses Probabilistic Separation Logic and develops it with new semantics for the programming language and logic formulas together with a new frame rule. Types are added to the syntax. For the semantics of the programming language the monadic denotational semantics is used. It requires domain theory which is also briefly presented. The logic is expanded with a third truth value — undefined. The frame rule is significantly simplified with the removal of side conditions. The correctness of the simplified version of the frame rule is proved. The use of logic is presented on examples of cryptographic protocols. separacijska logika denotacijska semantika trovrednostna logika tipni sistem verjetnostno programiranje dokazovanje pravilnosti verjetnostna neodvisnost separation logic denotational semantics three-value logic type system probabilistic programming proving program correctness probabilistic independence true false false Slovenski jezik Angleški jezik Diplomsko delo/naloga 2025-07-03 16:19:27 2025-07-03 16:19:29 2025-07-04 11:14:16 0000-00-00 00:00:00 2025 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 38146 241427715 Jereb_Janez_ignacij_-_Verjetnostna_separacijska_logika.pdf Jereb_Janez_ignacij_-_Verjetnostna_separacijska_logika.pdf 1 F1EE653EA99183952F745654D7829B88 d3b36a68661e28a883da975bab9a7596f56e33d5eccde682c6a69a7183a3a321 d4682caa-5816-11f0-b232-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=212327 Fakulteta za računalništvo in informatiko 0 0 0