Preliminary Materials

  • RoboStar framework for design and verification of robotic systems

    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.

  • An introduction to modelling and verification in Isabelle/HOL

    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/.

Videos and Slides