Committee

  • Zak Kincaid (advisor)
  • David Walker
  • Aarti Gupta

Title

A theory of non-linear integer arithmetic

Abstract

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.

Reading List

Papers

  1. A Survey of SMT, David Monniaux. (link)
  2. Software model-checking. (link)
  3. Computing a Groebner basis of a polynomial ideal over an Euclidean domain. (link)
  4. An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints. (link)
  5. Solving Nonlinear Integer Arithmetic with MCSAT. (link)
  6. Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. (link)

Textbooks

  1. Calculus of Computations. (link)
  2. Principles of Program Analysis, Chapter 4. (link)
  3. Ideals, Varieties and Algorithms (Chapters 1 - 4). (link)
  4. Theory of Integer and Linear Programming, Alexander Schrijver

Questions

(including follow-up questions)
  1. (Walker) Define what abstract interpretation is. What does it require? What is a Galois connection and simulation relation? Give an example of an abstract interpretation.
  2. (Kincaid) What is a Craig interpolant? What is an application? Can you give an example of that and show it in a program? (Predicate abstraction.) How do you compute the interpolants? Does your theory admit quantifier-free interpolants?
  3. (Gupta) Explain what DPLL(T) is. What makes modern DPLL solvers successful? Does your solver do theory clause learning or theory propagation? How can you extend your solver to do that? How can your solver handle instances that are actually SAT but deemed UNSAT? What does CPAChecker do?
  4. (Walker) Summarize the contributions and ideas of Tiwari's paper, and why you liked it. What's a certificate for unsatisfiability?