Navrhujeme reseni automaticke extrakce verifikacnich modelu pro zdrojove kody v jazyku C. Primarne se zamerujeme na reprezentaci ukazatelu a poli, coz cini extrakci z jazyka C specifickou.