Formální verifikace je soubor metod, pomocí nichž je možné ověřit, že implementace softwaru odpovídá formální specifikaci očekávaného chování nebo splňuje specifické vlastnosti (chybové stavy jsou nedosažitelné, vlákna se nikdy nedostanou do deadlocku apod.). Formální verifikace je považována za nejvyšší stupeň záruk spolehlivosti softwaru, protože na rozdíl od běžnějších metod (jako třeba testování) je "úplná" - dává vyčerpávající matematický důkaz o správnosti softwaru v daném kontextu.

Během jedné hodiny pochopitelně nebude možné obsáhnout otázku formální verifikace v celé šíři a s veškerou teorií, ale ukážeme si na praktických příkladech postup a záludnosti formální verifikace funkcionálního kódu reálných projektů: mikrojádra seL4 (Haskell, Isabelle/HOL) a kryptografické knihovny miTLS (F#, F7, F*).

Na sraz se prosím registrujte na https://www.meetup.com/FSharping/events/238948997/

www.pracovna.cz