ECNU-SEI-SUMMERSCHOOL2022

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

RoboStar framework for design and verification of robotic systems
Slides: RoboStar-slides | RoboStar-Practical | practical3-solutions.pdf | materials for friday.zip
Videos: RoboStar-videos
问答工具：https://uniofyork.padlet.org/anacavalcanti7/Portfolio
投票工具：https://www.menti.com/nwgmr4o451
An introduction to modelling and verification in Isabelle/HOL
Slides: Lectures | JW-Logic-Slides.zip
Functional Overapproximation for Reachability Analysis of Neural Network Control Systems
Slides: Lecture_0 | Lecture_1 | Lecture_2 | Lecture_3
Models: cruise_control.m | quadrotor.m | spring_pendulum.m

RoboStar framework for design and verification of robotic systems
Homework1: Practical-1-no-sols
link: https://pan.quark.cn/s/ceb9c60b52b6