The Young Software Engineer’s Guide to Using Formal Methods

Cancelled
Event details
Date | 08.06.2018 |
Hour | 13:30 › 14:15 |
Location | |
Category | Conferences - Seminars |
By Prof. K. Rustan M. Leino
Abstract
If programming was ever a hermitlike activity, those days are in the past. Like other internet-aided social processes, software engineers connect and learn online. Open-source repositories exemplify common coding patterns and best practices, videos and interactive tutorials teach foundations and pass on insight, and online forums invite and answer technical questions. These knowledge-sharing facilities make it easier for engineers to pick up new techniques, coding practices, languages, and libraries. This is good news in a world where software quality is as important as ever and where formal verification tools have become practically feasible.
In this talk, I give one view of the future of software engineering, especially with an eye toward software quality. I will survey some techniques, look at the history of tools, and inspire with some examples of what can be daily routine in the lives of next-generation software engineers.
Bio
Dr. K. Rustan M. Leino is a Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He is known for his work on formal methods and programming languages. He has a long history of building program verifiers for both mainstream languages and languages designed to enhance reasoning. His easy-to-use language and verifier Dafny are used in teaching at dozens of universities. Previously, Leino has held positions at Microsoft, Imperial College London, and DEC/Compaq. He has been named an ACM Fellow for his contributions to making program verification accessible and practical.
More information
Abstract
If programming was ever a hermitlike activity, those days are in the past. Like other internet-aided social processes, software engineers connect and learn online. Open-source repositories exemplify common coding patterns and best practices, videos and interactive tutorials teach foundations and pass on insight, and online forums invite and answer technical questions. These knowledge-sharing facilities make it easier for engineers to pick up new techniques, coding practices, languages, and libraries. This is good news in a world where software quality is as important as ever and where formal verification tools have become practically feasible.
In this talk, I give one view of the future of software engineering, especially with an eye toward software quality. I will survey some techniques, look at the history of tools, and inspire with some examples of what can be daily routine in the lives of next-generation software engineers.
Bio
Dr. K. Rustan M. Leino is a Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He is known for his work on formal methods and programming languages. He has a long history of building program verifiers for both mainstream languages and languages designed to enhance reasoning. His easy-to-use language and verifier Dafny are used in teaching at dozens of universities. Previously, Leino has held positions at Microsoft, Imperial College London, and DEC/Compaq. He has been named an ACM Fellow for his contributions to making program verification accessible and practical.
More information
Practical information
- General public
- Free
Contact
- Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch