DIKU Bits: VeriMon - A Verified Monitoring Tool

Portrait Dmitriy TraytelSpeaker

Dmitriy Traytel, Associate Professor at the Software, Data, People & Society Section at DIKU.


In runtime verification, monitoring is the task of detecting whether a system execution adheres to given rules. Runtime monitors are used in safety- and security-critical applications, where errors are too costly to be tolerated. Their correctness is important and rarely obvious. VeriMon is a monitor whose correctness has been formally verified in the Isabelle proof asistant. I will talk about VeriMon's evolution and demonstrate how it helped detect genuine errors in other unverified monitors.  

Zooming in on Dmitriy Traytel  

Which courses do you teach?  
I am new to DIKU and for now only the MSc course I will be teaching together with Yongluan Zhou in Block 2 has been fixed: Advanced Computer Systems. In this course, we teach how to design distributed systems that are performant, scalable, and correct.  

Which technology/research/projects/startup are you excited to see the evolution of?  
Proof assistants. These are tools that mechanically check human-written formal proofs, e.g., of an algorithm's correctness, and support their users in developing these proofs. Landmark achievements in this area include realistic verified compilers and operating system kernels. My research goal is to make proof assistants so expressive and easy to use that such verifications will become commonplace.  

What is your favorite sketch from the DIKUrevy?  
I had to do some research on its YouTube channel to learn about DIKUrevy. There, I could relate to "Bruger Vi ML" best. The Isabelle proof assistant is implemented in Standard ML.