Title: GIMPLE Model Checker Author: Ondrej Krč-Jediný Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Ondřej Šerý Ph.D. Supervisor's e-mail address: Ondrej.Sery@mff.cuni.cz The goal of the thesis is a prototype implementation of explicit-state model checker of C - an advanced tool for finding errors in programs. This tool ex- plores all possible paths of program execution as well as all thread interleavings. It is based on GIMPLE - output of front-end of GCC compiler, which is the input language for GMC. The thesis is based on the previous work 'Memory represen- tation for GIMPLE Model Checker', that implements work with memory for this tool. Since it is based on GIMPLE, it makes it possible to verify systems directly in C. In addition, it is easily extensible to other languages supported by GCC. Keywords: model checking, GIMPLE, GCC, C 1