Skip to main content

Separation Logic in SMT Solvers


Suitable for

MSc by Research
MSc in Computer Science


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.