We have seen much progress in (automated) program verification techniques and a few successful verification tools in the past few decades. Still, program verification is not as widely adopted as I hoped.

In this talk, I will discuss my experience in developing theories and tools for type-based program verification, perspectives on what hampers the broad adoption of formal verification, and a few half-baked ideas of how we might overcome the problem so that everyone can get (the benefits of) verification.

Atsushi Igarashi is a Professor at Dept. of Communication and Computer Engineering, Graduate School of Informatics, Kyoto University. He received his PhD degree from the University of Tokyo in 2000. His research interest is in principles of programming languages, in particular, type systems and program verification. He received the AITO Dahl-Nygaard Junior Prize in 2011 for his contribution to the foundations of object-oriented languages with his work on Featherweight Java and its extensions.