This repository serves as a learning ground for using separation logic with low level programming languages. I don't really know much about it so here is my current game plan. This will likely changes as I learn more.
For anything that is a Software Foundations book I will leave out solutions to the exercises at the authors requests.
- read preface.v and follow preperation suggestions
- You will also need a working knowledge of the C programming language.
- Study Software Foundations Volume 1 (Logical Foundations)
- Study the Hoare and Hoare2 chapters of Software Foundations Volume 2 (Programming Language Foundations), and do the exercises!
- Study the Sort, SearchTree, and ADT chapters of Software Foundations Volume 3 (Verified Functional Algorithms), and do the exercises!
- install vst tool chain
- Complete the Software Foundation Volume 4