Verification of C programs is an active research field with many tools competing at an annual competition on software verification (SV-COMP) . Korn  is a prototype software verifier for C programs, which translates C programs into a system of constrained Horn clauses. The generated Horn clauses are then passed to a dedicated Horn solver, which does all the hard work. Korn currently supports control-flow analysis, including loops and functions. The goal of this project is to implement proper support for arrays, which is now very limited in Korn.