Učitavanje video playera...
00:59:54
Marko Doko: Separacijska logika za obećavajuću semantiku
Sažetak: U prvom dijelu seminara, prezentirat ćemo "obećevajuću semantiku" (eng. promising semantics) [1]. Radi se o semantici izvršavanja višenitnih programa koja izbjegava tzv. out-of-thin-air problem (situacija kada semantika dozvoljava da program proizvodi vrijednosti koje nigdje nisu unesene). Vidjet ćemo zbog čega semantike u stilu C/C++ 11 standarda nisu u mogućnosti riješiti taj problem i kako alternativni pristup obećavajuće semantike daje kvalitetne rezultate.
U drugom dijelu seminara prezentirat ćemo separacijsku logiku SLR [2]. Radi se o prvoj separacijskoj logici koja je valjana za obećavajuću semantiku. Kako je obećavajuća semantika podosta inovativan semantički model, za dokaz valjanosti bila je potrebna nova tehnika dokazivanja.
