Modex is a tool that can be used to mechanically extract high-level verification models from implementation level C code. Modex itself is written in ANSI-C, and its application domain is also restricted to ANSI-C code. The generated verification models are gvien in Promela, for input to the SPIN model checker. In the seminar, I will give an introduction to how it works, how it can be used, and what can be accomplished. The main purpose is to give a glimpse of how tools for software verification could work. If time and preparation permits, I may also say a few words about BLAST, another tool formodel checking of C code. You can find the ModEX WWW page here.