Proving correctness of Java programs
using higher order separation logic
- Speaker
Jesper Bengtson, IT-University of Copenhagen, Denmark
- Date and Time
Tuesday, September 20th, 2011, (time: 10:15-12.00)
Thursday, September 22nd, 2011, (time: 13:15-15.00)
- Location
Polacksbacken, room 1212
- Abstract
In these two lectures I will discuss current work at the IT-University of Copenhagen where we aim to prove correctness of Java programs using higher order separation logic. The first lecture will be an introductory lecture to separation logic. I will cover the basics -- no previous knowledge in the area is required, although some rudimentary experience with Hoare logic is beneficial. In the second lecture I will cover how to use higher order separation logic to verify Java programs. In particular I will discuss the approach we use to write program specifications and how we reason about inheritance.