DIKU IT-C RUC

COPLAS

Copenhagen Programming Language Seminar


Certifying algorithms for Unit Two Variable Per Inequality (UTVPI) constraints (CANCELED)

K. Subramani
West Virginia University

Thursday, August 16th, 2012, 15:00 - 16:00
DIKU, Universitetsparken 1, Meeting room A+B

Abstract:

In this talk, I will discuss the design and analysis of time-optimal and space-optimal, certifying algorithms for checking the linear and lattice point feasibility of a class of constraints called Unit Two Variable Per Inequality (UTVPI) constraints. In a UTVPI constraint, there are at most two non-zero variables per constraint, and the coefficients of the non-zero variables belong to the set $\{+1,\ -1\}$. These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. As per the literature, the fastest known certifying algorithm for checking lattice point feasibility in UTVPI constraint systems, runs in $O(m \cdot n+n^{2} \cdot \log n)$ time and $O(n^{2})$ space, where $m$ represents the number of constraints and $n$ represents the number of variables in the constraint system. We shall present new algorithms for checking the linear feasibility and the lattice point feasibility of UTVPI constraints. Both of the presented algorithms run in $O(m \cdot n)$ time and $O(m+n)$ space. Additionally they are certifying in that they produce satisfying assignments in the event that they are presented with feasible instances and refutations in the event that they are presented with infeasible instances. The importance of providing certificates cannot be overemphasized, especially in mission-critical applications. Our approaches for both the linear and the lattice point feasibility problems in UTVPI constraints are fundamentally different from existing approaches, in that our approaches are based on new inference rules.


Scientific host: Fritz Henglein Administrative host:Jette Møller. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, DTU, ITU, and RUC.
COPLAS is part of the FIRST Research School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org