Solving Non-linear Arithmetic with SAT-based Model Checking

This saminar introduces a decision procedure for leveraging model checking with enhanced efficiency for solving Non-linear Integer Arithmetic (NIA). Traditional approaches, predominantly reliant on bit-blasting and a mix of bit-blasting with theory reasoning, falter under the weight of non-linear operations like multiplication and division due to scalability issues.
We propose an alternative strategy that reduces NIA satisfiability into a model checking problem. Our approach uniquely addresses the complexities of non-linear operations by devising tailored abstraction-refinement techniques.

M.Sc. student under the supervision of Prof. Yakir Vizel.