There have been 1 topic suggestion tagged with model checking.
Automated Verification of Computational Systems
It was realized in the 1960s that mathematical logic provides a suitable language to formulate properties of programs. This idea was formalized by Hoare who developed Hoare logic as a means to prove program correctness. However, this technique didn't apply directly to concurrent programs. An alternative approach called Temporal Logic was proposed by Amir Pneuli in 1977 which did provide a means to reason about concurrent programs. This topic studies this and then delves into the fundamental ideas behind model checking.
Required Background: Basics of computer science at the level of CS 146, Logic at the level of CS 245.
Possible reference materials for this topic include
Grumberg, O., & Veith, H. (Eds.). (2008). 25 years of model checking: history, achievements, perspectives (Vol. 5000). Springer.
Quick links: Google search, arXiv.org search, propose to present a talk
computer science logic model checking