Title: Directions to and for verified software
Speaker: K. Rustan M. Leino (Amazon)
Date: Monday, October 16 th 2017
Where: Faculty of Informatics, Ada Lovelace Room (UPV/EHU)
Organizers: Grupo LoRea & UFI Bailab
There are many techniques and tools aimed at creating and maintaining reliable software. At one extreme is deductive verification, where software designers write specifications for what the software is supposed to do and where programs are developed together with proofs that show the specifications are met. Research and development behind deductive verification have been a long journey, from early visions of the idea, through criticism and doubt, through the development of automated techniques, to education, to experience in using the tools in practice, and to streamlining of the process. In this talk, I will describe where research in program verification has brought us today, give a demo of the state-of-the-art system Dafny for writing verified programs, and discuss directions for what may be possible in the future.
K. Rustan M. Leino is Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He is known for his work
on programming methods and program verification tools, and is a world leader in building automated program verification tools. These
include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.
He is an ACM Fellow.
Before Amazon, Leino has worked as Principal Researcher at Microsoft Research, a Visiting Professor at Imperial College London, and a
researcher at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software
as a technical lead in the Windows NT group at Microsoft. Leino hosts the Verification Corner channel on youtube. He is a multi-
instrumentalist, he instructed group cardio and strength classes for many years, and he likes to cook.