Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Mon 16 Jan 2017 11:00 - 11:30 at Amphitheater 44 - Numerical domains Chair(s): Laure Gonnord

Polyhedra are used in verification and automatic parallelization to capture linear relations between variables. A polyhedron can be represented as constraints, generators or both in the double description framework. Whatever the representation, most polyhedral operators spend a significant amount of time to maintain minimal representations.

To minimize a polyhedron in constraints-only representation, the redundancy of each constraint must be checked with respect to others. Each of these redundancy tests generally implies solving a linear programming (LP) problem using the simplex algorithm. We present an algorithm that replaces most LP problem resolutions by distance computations.

The geometric intuition is simple: consider ray traces starting from a point within the polyhedron and orthogonal to its faces. A face first encountered by one of these rays is an actual face of the polyhedron. It is therefore a non-redundant constraint. Since this procedure is incomplete, LP problem resolutions are required for the remaining undetermined constraints.

Experiments show that our algorithm drastically reduces the number of calls to the simplex, resulting in a considerable speed improvement. In addition, our algorithm generates by construction a certificate for each constraint: redundancy is established by exhibiting a non-negative linear combination of contraints that yields the removed constraint, whereas irredundancy is shown by exhibiting a point outside of the polyhedron which is excluded only by the kept constraint.

To follow the geometric interpretation, the algorithm is explained in terms of constraints but it can also be used to minimize generators.

slides (Marechal_VMCAI2017.pdf)885KiB

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Numerical domainsVMCAI at Amphitheater 44
Chair(s): Laure Gonnord University of Lyon & LIP, France
10:30
30m
Talk
Sound Bit-Precise Numerical Domains
VMCAI
Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
File Attached
11:00
30m
Talk
Efficient Elimination of Redundancies in Polyhedra using Raytracing
VMCAI
Media Attached File Attached
11:30
30m
Talk
Finding Relevant Templates via the Principal Component Analysis
VMCAI
Yassamine Seladji University of Tlemcen
File Attached