Program Verification

Date: October 2

Time: 11am

Room: BBL-505

Speaker: Wishnu Prasetya

Title: Program Verification

Abstract

Thanks to computers, our modern society is able to multiply its productivity to a revolutionary level. The other side of this is that software have become increasingly complicated, making it more difficult to keep them reliable, and that we start to rely too much on them, which makes software reliability a critical factor. Subjecting programs to heavy testing helps, but in the end, there is only so much we can do with testing. Testing is simply fundamentally inadequate, especially to handle crititical and delicate programs. Program verification is, one can say, a mathematical approach of testing a program. It is based on a mathematical approach. It is expressive and accurate, but it is also very expensive. It is an emerging field, with lots of research currently invested to bring down the cost. In this talk I will show you some basic principles in program verification, and two complementary techniques which are used a lot nowadays: theorem proving and model checking.