Seminar: Graduate Seminar

ECE Women Community

Solving Non-linear Arithmetic with SAT-based Model Checking

Date: June,23,2024 Start Time: 10:00 - 11:30
Location: 608, Zisapel Building
Add to:
Lecturer: Eliezer Almog Zaffrani

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.


All Seminars
Skip to content