2014

2015

2016

2017

2018

2019

2020

2022

2023

2024

The forty-fourth meeting of the Prague computer science seminar

Jan Vítek

Reasoning about programs: Soundness revisited

This talk will overview the foundations of program analysis; which started 50 years ago with data flow analysis and abstract interpretation. Advancing through the years, we will touch on some key techniques and discuss their practical implications. We will conclude with a look at unsound techniques, explain the sources of unsoundness and what can be done to mitigate it.

Annotation Lecturer

2024
2023
2022
2020
2019
2018
2017
2016
2015
2014

Play record

October 17, 2019

4:15pm

Auditorium S5, MFF UK
Malostranské nám. 25, Praha 1
Show on the map

Information security, software assurance, and program performance all crucially depend on our ability to reason formally about possible program behaviors. Determining if a particular function will reveal a password, avoiding code that crashes embedded devices, and applying transformations that provide an order-of-magnitude speed up, are all tasks that require treating the code as an object of analysis on which we can perform meaning-preserving transformations.

This talk will overview the foundations of program analysis; which started 50 years ago with data flow analysis and abstract interpretation. Advancing through the years, we will touch on some key techniques and discuss their practical implications. We will conclude with a look at unsound techniques, explain the sources of unsoundness and what can be done to mitigate it.

Jan Vítek

Jan Vitek is a Professor of Computer Science at the Northeastern University (Boston, USA) and an ERC grant holder at the Czech Technical University. He holds degrees from the University of Geneva (PhD'99, BS'89) and University of Victoria (MS'95). Professor Vitek works on topics related to the design and implementation of programming languages. In the Ovm project, he led the implementation of the first real-time Java virtual machine to be successfully flight-tested. Together with Noble and Potter, he proposed a concept that became known as Ownership Types. Prof Vitek was one of the designers of the Thorn language. He works on gaining a better understanding of the JavaScript language and is now looking at supporting scalable data analysis in R. Prof. Vitek chaired ACM SIGPLAN; he was the Chief Scientist at Fiji Systems, part of the founding team at H2O.ai, a vice chair of AITO, and a vice chair of IFIP WG 2.4. He chaired SPLASH, PLDI, ECOOP, ISMM and LCTES conferences and was program chair of ESOP, ECOOP, VEE, Coordination, and TOOLS.

Its program consists of a one-hour lecture followed by a discussion. The lecture is based on an (internationally) exceptional or remarkable achievement of the lecturer, presented in a way which is comprehensible and interesting to a broad computer science community. The lectures are in English.

The seminar is organized by the organizational committee consisting of Roman Barták (Charles University, Faculty of Mathematics and Physics), Jaroslav Hlinka (Czech Academy of Sciences, Computer Science Institute), Michal Chytil, Pavel Kordík (CTU in Prague, Faculty of Information Technologies), Michal Koucký (Charles University, Faculty of Mathematics and Physics), Jan Kybic (CTU in Prague, Faculty of Electrical Engineering), Michal Pěchouček (CTU in Prague, Faculty of Electrical Engineering), Jiří Sgall (Charles University, Faculty of Mathematics and Physics), Vojtěch Svátek (University of Economics, Faculty of Informatics and Statistics), Michal Šorel (Czech Academy of Sciences, Institute of Information Theory and Automation), Tomáš Werner (CTU in Prague, Faculty of Electrical Engineering), and Filip Železný (CTU in Prague, Faculty of Electrical Engineering)

The idea to organize this seminar emerged in discussions of the representatives of several research institutes on how to avoid the undesired fragmentation of the Czech computer science community.