There is plenty of material at https://robostar.cs.york.ac.uk/, including information to download and install RoboTool, which will be presented in the course.
Students are recommended to read Part I of the book Concrete Semantics by Nipkow & Klein. This contains a self-contained introduction to the Isabelle proof assistant. The book can be downloaded from http://concrete-semantics.org/.
Slides: RoboStar-slides |
materials for friday.zip