University of Oxford Logo University of OxfordDepartment of Computer Science - Home

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.