Skip to main content

Separation Logic in SMT Solvers

Supervisor

Suitable for

MSc by Research
MSc in Computer Science

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.