University of Cambridge
4pm Tuesday 13th May 2008
Room 2511, JCMB, King's Buildings
In OO programs inheritance is used to provide a flexible method for creating new classes from old ones. However, typically when verifying programs the flexibility of inheritance lost. In this talk, I will provide three examples of inheritance (the good, the bad, and the ugly), and I will explain how these cause problems for standard verification schemes. I will then build on our previous work and develop a modular verification method for OO programs that allows these different examples of inheritance to be verified.
This is joint work with Gavin Bierman and appeared at POPL 2008.