Abstract: Disjunctive linear arithmetic (a Boolean combination of inequalities of the form Σa_i * x_i < b_i, where for all i, a_i, b_i are constants, and x_i is of type Real, e.g., 2x + 3y -5z < 2) is a major decidable theory that is frequently used in formal verification of both hardware designs and software. We show a reduction from disjunctive linear arithmetic to propositional logic, based on the Fourier-Motzkin elimination technique. While the complexity of this procedure is not better than competing techniques, it has practical advantages in solving verification problems. It also promotes the option of deciding a combination of theories by reducing them to this logic. The talk will include a survey of existing approaches and a comparison between them.

Short CV: Ofer Strichman Received his B.Sc and M.sc from the Technion in Operations Research and System Analysis, and his Ph.D in Computer Science from the Weizmann Institute (Israel). His Ph.D. thesis, under the guidance of Prof. Amir Pnueli, covered various subjects in formal verification like Translation Validation, decision procedure for Equality Logic and Bounded Model Checking. He is currently a post-doc in Prof. Ed Clarke's group.