The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Separation logic has been used successfully to verify safety properties of programs which manipulate the heap. The Smallfoot family of program analysers are capable of verifying shape properties of pointer programs, for example analysing the shape of inductive structures on the heap, such as linked lists. I discuss an extension to this work which concerns the automatic verification of functional properties of pointer programs. I will discuss the challenging parts of such verifications which require creative input. The talk will be motivated by examples and possibly a working demo of some of the early results.