[Proof Complexity] Seminar Fri Aug 27 at 10:00 CEST with Dmitriy Traytel: Who is Isabelle, and why is she so picky about my proofs?

[Jakob Nordström]

Dear all,

On Friday August 27 at 10:00 we are having the first seminar for the autumn in the MIAO video seminar series. Dmitriy Traytel from the University of Copenhagen will tell us about who Isabell is, and why she is so picky about proofs. See below for the abstract.

We will meet virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming video seminars can be found at http://www.jakobnordstrom.se/videoseminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jakob.nordstrom at cs.lth.se.

Best regards,
Jakob Nordström

**********

Friday Aug 27 at 10:00
Who is Isabelle, and why is she so picky about my proofs?
(Dmitriy Traytel, University of Copenhagen)

Proof assistants 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, operating system kernels, and distributed systems as well as formal proofs of deep mathematical results such as the four color theorem, the Feit–Thompson theorem, and the Kepler conjecture. In this talk, I will give a brief introduction of the Isabelle/HOL proof assistant, of which I am both a user and a developer. I will explain how Isabelle's foundational approach achieves the highest level of trustworthiness and will examplify the benefits of using a proof assistant via three case studies: the formal verification of security properties of authenticated data structures, the completeness of ordered resolution, and the correctness of an efficient runtime monitoring algorithm.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se