Description

Program verification with VerCors relies on SMT solvers such as Z3 to compute whether or not formulas hold. SMT solvers are good at solving boolean and simple arithmetic. However, when non-linear arithmetic is used, such as multiplication or modulo, proving programs correct becomes difficult. Furthermore, support for non-linear arithmetic is often not directly usable.

The goal of this project is to determine the limits of and tuning needed to use the non-linear arithmetic support in SMT solvers with VerCors.
This is done through the following steps:

• Study papers documenting support for non-linear arithmetic in SMT solvers
• Document the kinds of non-linear arithmetic that are supported and their limits
• Find, and possibly design, examples to test the non-linear capabilities of SMT solvers
• Categorize and benchmark the different flags, options, and their values, for tuning non-linear arithmetic solving.