Nicolas Koh will present his General Exam "A theory of non-linear integer arithmetic" on May 3, 2022 at 3pm in CS 302 and via Zoom
The members of his committee are as follows: Zak Kincaid (adviser), David Walker, Aarti Gupta
A theory of non-linear integer arithmetic
Inferring and verifying non-linear arithmetic invariants in programs is fundamentally challenging not only because of high computational complexity, but in the case of integers, the theory is not even recursively axiomatizable. Nevertheless, invariants that arise in practice and the attendant reasoning involved may be far more tractable. In this talk, we give an axiomatization of a “weak” theory of non-linear integer arithmetic, and show how satisfiability for this theory can be decided using a mix of polynomial algebra and polyhedral geometry. At heart, the axioms enable the reduction of non-linear arithmetic to the linear setting, allowing standard techniques to be employed.