A hallgató feladata, hogy a félév során megismerkedjen a programhelyesség bizonyításának elméleti oldalával, illetve a megszerzett ismereteket C nyelven írt algoritmusok parciális helyességének bizonyítására alkalmazza. A keletkezett formulák kiértékeléséhez a Microsoft Research által fejlesztett Z3 theorem prover kerülne felhasználásra.

A feladat célja egy automatizált az programhelyesség bizonyító keretprogram alapjainak az elkészítése, és az ismertetett módszer gyakorlati alkalmazhatóságának a bemutatása