« BACK TO PROGRAM

Trends in automated verification

K. Rustan M. Leino - Amazon

Mechanized support for formally verifying programs has undergone dramatic improvements in the last couple of decades. Tools now offer more automation and are easier to use than ever before. The languages and specifications used as input to automated verifiers are also becoming more powerful and expressive. In this talk, I will give some history leading to the current state of automated verifiers, and will demonstrate some advanced applications of such tools.

Download this presentation

About K. Rustan M. Leino

Dr. K. Rustan M. Leino is a Senior Principal Engineer in the Automated Reasoning Group at Amazon. He is known for his work on formal techniques and tools for verifying software correctness. These include the languages and tools ESC/Java, Houdini, Spec#, Boogie, Chalice, and Dafny. Leino has been recognized as an ACM Fellow for "contributions to making program verification practical and accessible".