# Separation Logic Course

This webpage provides material for the second part of Course 2-36-1 "Proof of Program", MPRI 2018-2019. (Material for the first part can be found on François Bobot's webpage). This second part teaches fundamentals of separation logic and the corresponding proof methods.

## Plan

• Introduction
slides
• Lecture 1 (January 14):
basic heap predicates, mutable lists and trees, list segments, structures with sharing, specification triples.
slides, exam 2014 (exercise 2)
• Lecture 2 (January 28):
frame rule, small footprint specifications, heap entailment, structural rules, reasoning rules for terms.
slides, exam 2015 (exercise 2)
• Lecture 3 (February 4):
loops, aliasing and local state, higher-order iterations specification of higher-order functions, characteristic formulas.
slides
• Lecture 4 (February 11):
characteristic formulas with structural rules, higher-order representation predicates and iteration, resource analysis, permissions, parallelism and concurrency.
slides

## Previous exams

You may have a look at the exam for 2016-2017. You may even look at some of the solutions, once you actually had a serious go at the exercises.

Previous exams:

## Installation instructions for interactive proofs

```# STEP 1 (~15 minutes)
# if you don't have it, install opam with ocaml 4.05.0

sudo apt-get install unzip m4 aspcud
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
eval `opam config env`
opam switch 4.05.0 # should be the default switch anyway
eval `opam config env`

# STEP 2 (~40 minutes)
# if you don't have it, install Coq 8.6.1
# (Coq 8.7.0 and Coq 8.7.1 work as well)

opam install coq.8.6.1

#if you want coqide and run into problem, try installing libgtksourceview2.0-dev and then coqide
sudo apt-get install libgtksourceview2.0-dev
opam install coqide

# STEP 3 (~1 minute)

mkdir mpri_sep_course
cd mpri_sep_course
unzip sepcourse.zip
make -j # this should fail for file Repr.v

# STEP 4
# play with Hprop.v and then Repr.v

coqide Hprop.v
coqide Repr.v
# you can run emacs instead of coqide if you have with proof general installed
```