2014
2015
2016
2017
2018
2019
2020
2022
2023
2024

Čtyřicátéčtvrté setkání Pražského informatického semináře

Jan Vítek

Jak analyzovat korektnost programů

V přednášce stručně představíme základy analýzy programů, počínaje analýzou toku dat a metodou abstraktní interpretace, které byly vytvořeny před více než 50 lety. Popíšeme i některé novější techniky a jejich praktické důsledky. Nakonec zmíníme i postupy nekorektní, vysvětlíme důvody jejich nekorektnosti a to, jak zmírnit její následky.

17. října 2019

16:15

Posluchárna S5, MFF UK
Malostranské nám. 25, Praha 1
Zobrazit na mapě

Anotace přednášky

Pro poskytování záruk týkajících se správnosti, bezpečnosti a výkonu software je nutné umět formálně analyzovat možná chování programu. Určit, jestli daná funkce umožní útočníkovi zjistit heslo, zamezit selhání vestavěného řídícího systému, či aplikovat transformace umožňující řádové zrychlení výpočtu, to jsou příklady úloh, které vyžadují analyzovat kód jako objekt, na kterém je možné provádět transformace zachovávající význam kódu.

V přednášce stručně představíme základy analýzy programů, počínaje analýzou toku dat a metodou abstraktní interpretace, které byly vytvořeny před více než 50 lety. Popíšeme i některé novější techniky a jejich praktické důsledky. Nakonec zmíníme i postupy nekorektní, vysvětlíme důvody jejich nekorektnosti a to, jak zmírnit její následky.

Přednášející

Jan Vítek

Jan Vítek je profesorem informatiky na Northeastern University a držitelem ERC grantu na Českém vysokém učení technickém v Praze. Je držitelem titulů z univerzity v Ženevě (PhD 1999, BS 1989) a v kanadské Victorii (MS 1995). Profesor Vítek pracuje na tématech spojených s navrhováním a implementací programovacích jazyků. V projektu Ovm vedl implementaci virtuálního stroje pro jazyk Java pracujícího v reálném čase. Společně se svými kolegy J. Noblem a J. Potterem navrhl koncept tzv. “typů vlastnictví”. Prof. Vítek byl jedním z tvůrců jazyka Thorn, pracuje na lepším pochopení podstaty jazyka JavaScript a zabývá se podporou škálovatelné analýzy dat v jazyce R. Prof. Vítek předsedal konferenci ACM SIGPLAN; byl vedoucím vědcem ve firmě Fiji Systems, součástí zakládajícího týmu firmy H2O.ai, místopředsedou organizací AITO a IFIP WG 2.4. Předsedal konferencím SPLASH, PLDI, ECOOP, ISMM a LCTES a byl programovým předsedou konferencí ESOP, ECOOP, VEE, Coordination a TOOLS.

O PRAŽSKÉM INFORMATICKÉM SEMINÁŘI

Seminář se obvykle schází jednou za měsíc ve čtvrtek v 16:15 a to buď v budově FEL ČVUT nebo v budově MFF UK.

Jeho program je tvořen hodinovou přednáškou, po níž následuje časově neomezená diskuse. Základem přednášky je něco (v mezinárodním měřítku) mimořádného nebo aspoň pozoruhodného, na co přednášející přišel a co vysvětlí způsobem srozumitelným a zajímavým i pro širší informatickou obec. Přednášky jsou standardně v angličtině.

Seminář připravuje organizační výbor ve složení Roman Barták (MFF UK), Jaroslav Hlinka (ÚI AV ČR), Michal Chytil, Pavel Kordík (FIT ČVUT), Michal Koucký (MFF UK), Jan Kybic (FEL ČVUT), Michal Pěchouček (FEL ČVUT), Jiří Sgall (MFF UK), Vojtěch Svátek (FIS VŠE), Michal Šorel (ÚTIA AV ČR), Tomáš Werner (FEL ČVUT), Filip Železný (FEL ČVUT)

Idea Pražského informatického semináře vznikla z rozhovorů představitelů několika vědeckých institucí na téma, jak odstranit zbytečnou fragmentaci informatické komunity v ČR.

Podporovatelé

Kontakt

Pražský informatický seminář je z důvodů prevence šíření nákazy novým koronavirem do odvolání pozastaven.