VESPA: Verified Stream Processing and Analytics

Speaker:
Dmitriy Traytel, ETH Zurich, Switzerland

Abstract:
The field of runtime verification, or monitoring, develops techniques to prove that a running system adheres to a formal specification. I work on the big data challenge in monitoring: how to make these techniques scale up to handle huge quantities of data, produced by today's large-scale systems? On the theoretical side, I develop new monitoring algorithms that have strict bounds on their memory consumption. On the practical side, I leverage existing big data technology, such as the Apache Flink framework, to parallelize existing state-of-the-art monitors, while retaining their correctness. My second passion, interactive theorem proving, is concerned with carrying out machine-checked proofs and developing proof assistants, the systems that check these proofs. I make proof assistants more expressive and easier to use. At the same time, I use proof assistants to prove correct complex algorithms from different domains, e.g., precisely the monitoring algorithms I develop. To join these two research directions and to develop trustworthy and scalable runtime verification tools, I plan to design and implement a new data stream processing framework, in the spirit of Apache Flink, in a proof assistant and formally verify the framework's fault-tolerance guarantees.

Biography:
Dmitriy Traytel is a senior researcher in David Basin's information security group at ETH Zürich. He completed his PhD in 2015 in Tobias Nipkow's logic and verification group at TU München. His general research goal is to develop methods for creating secure, trustworthy, and reliable software systems. His work towards this goal revolves around two topics in formal methods: runtime verification and interactive theorem proving.

Host: 

VESPA: Verified Stream Processing and Analytics
Contenuto:

Speaker:
Dmitriy Traytel, ETH Zurich, Switzerland

Abstract:
The field of runtime verification, or monitoring, develops techniques to prove that a running system adheres to a formal specification. I work on the big data challenge in monitoring: how to make these techniques scale up to handle huge quantities of data, produced by today's large-scale systems? On the theoretical side, I develop new monitoring algorithms that have strict bounds on their memory consumption. On the practical side, I leverage existing big data technology, such as the Apache Flink framework, to parallelize existing state-of-the-art monitors, while retaining their correctness. My second passion, interactive theorem proving, is concerned with carrying out machine-checked proofs and developing proof assistants, the systems that check these proofs. I make proof assistants more expressive and easier to use. At the same time, I use proof assistants to prove correct complex algorithms from different domains, e.g., precisely the monitoring algorithms I develop. To join these two research directions and to develop trustworthy and scalable runtime verification tools, I plan to design and implement a new data stream processing framework, in the spirit of Apache Flink, in a proof assistant and formally verify the framework's fault-tolerance guarantees.

Biography:
Dmitriy Traytel is a senior researcher in David Basin's information security group at ETH Zürich. He completed his PhD in 2015 in Tobias Nipkow's logic and verification group at TU München. His general research goal is to develop methods for creating secure, trustworthy, and reliable software systems. His work towards this goal revolves around two topics in formal methods: runtime verification and interactive theorem proving.

Host: Prof. Antonio Carzaniga