SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 04:00 - 04:20 at SPLASH-IV - Papers Chair(s): Liqian Chen, Khalil Ghorbal

Linear programming is a key technique for several numerical abstract domains, such as Template Constraint Matrix, constraint-only polyhedra, etc. However, most state-of-the-art linear programming solvers use floating-point arithmetic in their implementations, which can only give an approximate result that may be unsound (e.g., resulting in a larger value than the exact result for a minimization objective function). On the other hand, the solvers based on exact arithmetic are slow and have poor scalability. To this end, this paper aims at leveraging rigorous linear programming techniques which are built on the top of floating-point linear programming for soundly implementing numerical abstract domains. Particularly, in this paper, we present a new technique of rigorous linear programming which is based on Fourier-Mozkin elimination as a supplement to existing rigorous linear programming techniques. On the basis, we implement a tool, RlpSolver, combining Fourier-Mozkin elimination based and existing rigorous linear programming techniques together to lift effectiveness of rigorous linear programming in the scene of designing numerical abstract domains. Experimental results show that the new technique is complementary with existing rigorous linear programming techniques and their combination produces better results than a separate technique.

Tue 17 Nov

Displayed time zone: Central Time (US & Canada) change

03:00 - 04:20
PapersNSAD at SPLASH-IV
Chair(s): Liqian Chen National University of Defense Technology, China, Khalil Ghorbal Inria, France
03:00
20m
Paper
Abstract Domains for Constraint Programming with Differential Equations
NSAD
03:20
20m
Paper
Numeric Domains Meet Algebraic Data Types
NSAD
Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Thomas P. Jensen INRIA Rennes, BenoƮt Montagu Inria
03:40
20m
Paper
Proving array properties using data abstraction
NSAD
Julien Braine , Laure Gonnord University of Lyon & LIP, France
04:00
20m
Paper
Rigorous Linear Programming Techniques for Numerical Abstract Domains
NSAD
Tengbin Wang , Liqian Chen National University of Defense Technology, China, Ji Wang