Skip to main content
Department of Information Technology

Proving correctness of Java programs
using higher order separation logic


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)


Polacksbacken, room 1212


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.

Back to the seminar page

Updated  2011-09-19 10:08:22 by Frédéric Haziza.