Incorrectness Separation Logic with Borrows
Master Project of Matei Mirică

Project Description

This project investigates how to extend Incorectness Separation Logic with a formalism for the Borrows Aliasing Model for the purpose of detecting undefined behavior in Unsafe Rust.

Contacts for the Project

• Andreea Costea