Logical Investigations on Separation Logics

Topic: 
Logic & Computation
Level: 
Advanced
Abstract: 

Separation logic is a well-known formalism to extend Hoare logic to verify programs with pointers. In this course, we will investigate the logical side of separation logic by presenting material about models, decidability, computational complexity, expressive power and decision procedures, including those based on SMT solvers. We shall also provide some motivations behind the use of separation logic, chiefly related to its use in formal verification.

Week: 
Second week
Slot: 
09:00 - 10:30 - slot 1
Room: 
52.121