Separation Logic in SMT Solvers
Supervisor
Suitable for
Abstract
Reasoning about the heap is one of the biggest challenges in program analysis. The goal of this project is to evaluate ways of combining Satisfiability Modulo Theories with a decision procedure for a fragment of Separation Logic.