
COPLASCopenhagen Programming Language Seminar 
In this talk, I will discuss the design and analysis of timeoptimal and spaceoptimal, 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 nonzero variables per constraint, and the coefficients of the nonzero 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 missioncritical 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
proglangrequest@mail.itc.dk with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see
http://www.coplas.org