Array support in the Korn software verifier

Target

Research project

Contact

• Jan Kofroň
• Martin Blicha

Verification of C programs is an active research field with many tools competing at an annual competition on software verification (SV-COMP) [1]. Korn [2] 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.

1. https://sv-comp.sosy-lab.org/2023/index.php
2. https://github.com/gernst/korn