IC Colloquium : Directions to and for verified software
Event details
| Date | 06.03.2017 |
| Hour | 10:15 › 11:30 |
| Location | |
| Category | Conferences - Seminars |
By : Rustan Leino - Microsoft Research
Abstract :
There will always be computer programs whose behavior doesn't have to meet any particular expectations. But there is an increasing number of computer systems whose correct functioning affects our society: vehicular operations, secure transactions in web browsers, storage of medical information, digital currencies, etc. Luckily, there has also been progress in software development methods that can assist software engineers in producing verifiably correct software.
In this talk, I will describe where research in program verification has brought us today, give a demo of a state-of-the-art system for writing verified programs, and discuss directions for what may be possible in the future.
Bio :
Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. 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.
Prior to Microsoft Research, Leino worked 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 collects thinking puzzles on a popular web page and 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.
More information
Abstract :
There will always be computer programs whose behavior doesn't have to meet any particular expectations. But there is an increasing number of computer systems whose correct functioning affects our society: vehicular operations, secure transactions in web browsers, storage of medical information, digital currencies, etc. Luckily, there has also been progress in software development methods that can assist software engineers in producing verifiably correct software.
In this talk, I will describe where research in program verification has brought us today, give a demo of a state-of-the-art system for writing verified programs, and discuss directions for what may be possible in the future.
Bio :
Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. 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.
Prior to Microsoft Research, Leino worked 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 collects thinking puzzles on a popular web page and 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.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host : Jim Larus