Introduction to Seminar System Verification
![[TZI]](http://www.informatik.uni-bremen.de/~agbkb/images/buttons/TZI.gif)
![[BISS]](http://www.informatik.uni-bremen.de/~agbkb/images/buttons/BISS.gif)
Seminar: System Verification through Specification and Model-Checking
Hui Shi
Description:
This seminar covers verification of concurrent (parallel,
distributed und reactive) systems,
including real-time systems. Verification methods are discussed for
proving that such systems meet their specifications, with emphasis
on methods that combine model-checking techniques. For example,
CSP with the model-checker FDR, LTL (linear temperal logic) with
the model-checker SPIN and the SMV (symbolic machine verification)
system.
The seminar will comprise of a reading list (papers will be
collected and distributed to the class). Sutdents will be
expected to present one paper during the semester.
Folien: Introduction