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.

Anotace Přednášející Poster

2024
2023
2022
2020
2019
2018
2017
2016
2015
2014

Přehrát záznam

17. října 2019

16:15

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

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.

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.

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.