Document Open Access Logo

Making Rigorous Linear Programming Practical for Program Analysis

Authors Tengbin Wang, Liqian Chen, Taoqing Chen, Guangsheng Fan, Ji Wang

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.57.pdf
  • Filesize: 2.06 MB
  • 17 pages

Document Identifiers

Author Details

Tengbin Wang
  • College of Computer, National University of Defense Technology, Changsha, China
Liqian Chen
  • College of Computer, National University of Defense Technology, Changsha, China
Taoqing Chen
  • State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China
Guangsheng Fan
  • State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China
Ji Wang
  • State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China

Funding

This work is supported by the National Key R&D Program of China (No. 2017YFB1001802), and the National Natural Science Foundation of China (Nos. 61872445, 62032024).

Cite AsGet BibTex

Tengbin Wang, Liqian Chen, Taoqing Chen, Guangsheng Fan, and Ji Wang. Making Rigorous Linear Programming Practical for Program Analysis. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 57:1-57:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.57

Abstract

Linear programming is a key technique for analysis and verification of numerical properties in programs, neural networks, etc. In particular, in program analysis based on abstract interpretation, many numerical abstract domains (such as Template Constraint Matrix, constraint-only polyhedra, etc.) are designed on top of linear programming. However, most state-of-the-art linear programming solvers use floating-point arithmetic in their implementations, leading to an approximate result that may be unsound. On the other hand, the solvers implemented using exact arithmetic are too costly. To this end, this paper focuses on advancing rigorous linear programming techniques based on floating-point arithmetic for building sound and efficient program analysis. Particularly, as a supplement to existing techniques, we present a novel rigorous linear programming technique based on Fourier-Mozkin elimination. On this basis, we implement a tool, namely, RlpSolver, combining our technique with existing techniques to lift effectiveness of rigorous linear programming in the scene of analysis and verification. Experimental results show that our technique is complementary to existing techniques, and their combination (RlpSolver) can achieve a better trade-off between cost and precision via heuristic rules.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear programming
  • Software and its engineering → Formal methods
Keywords
  • Linear programming
  • rigorous linear programming
  • abstract interpretation
  • program analysis
  • Fourier-Mozkin elimination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. SI Bastrakov, AV Churkin, and N Yu Zolotykh. Accelerating fourier-motzkin elimination using bit pattern trees. Optimization Methods and Software, pages 1-14, 2020. Google Scholar
  2. Frédéric Besson. On using an inexact floating-point lp solver for deciding linear arithmetic in an smt solver. In 8th International Workshop on Satisfiability Modulo Theories, 2010. Google Scholar
  3. Liqian Chen, Antoine Miné, and Patrick Cousot. A sound floating-point polyhedra abstract domain. In Asian Symposium on Programming Languages and Systems, pages 3-18. Springer, 2008. Google Scholar
  4. Liqian Chen, Antoine Miné, Ji Wang, and Patrick Cousot. Interval polyhedra: An abstract domain to infer interval linear relationships. In International Static Analysis Symposium, pages 309-325. Springer, 2009. Google Scholar
  5. Sergei Nikolaevich Chernikov. The convolution of finite systems of linear inequalities. USSR Computational Mathematics and Mathematical Physics, 5(1):1-24, 1965. Google Scholar
  6. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238-252, 1977. Google Scholar
  7. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 84-96, 1978. Google Scholar
  8. Isil Dillig, Thomas Dillig, and Alex Aiken. Cuts from proofs: A complete and practical technique for solving linear inequalities over integers. In International Conference on Computer Aided Verification, pages 233-247. Springer, 2009. Google Scholar
  9. Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis, pages 269-286. Springer, 2017. Google Scholar
  10. Jared T Guilbeau, Md Istiaq Hossain, Sam D Karhbet, Ralph Baker Kearfott, Temitope S Sanusi, and Lihong Zhao. A review of computation of mathematically rigorous bounds on optima of linear programs. Journal of Global Optimization, 68(3):677-683, 2017. Google Scholar
  11. Christian Jansson. Rigorous error bounds for the optimal value of linear programming problems. In International Workshop on Global Optimization and Constraint Satisfaction, pages 59-70. Springer, 2002. Google Scholar
  12. P Kanniappan and K Thangavel. Modified fourier’s method of solving linear programming problems. Opsearch, 35(1):45-56, 1998. Google Scholar
  13. G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, 2017. Google Scholar
  14. Christian Keil. Lurupa-rigorous error bounds in linear programming. In Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2006. Google Scholar
  15. David A Kohler. Projections of convex polyhedral sets. Technical report, California Univ Berkeley Operations Research Center, 1967. Google Scholar
  16. Andrew Makhorin. Gnu linear programming kit. Moscow Aviation Institute, Moscow, Russia, 38, 2001. Google Scholar
  17. Alexandre Maréchal and Michaël Périn. Efficient elimination of redundancies in polyhedra by raytracing. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 367-385. Springer, 2017. Google Scholar
  18. David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. In International Conference on Computer Aided Verification, pages 570-583. Springer, 2009. Google Scholar
  19. Arnold Neumaier and Oleg Shcherbina. Safe bounds in linear and mixed-integer linear programming. Mathematical Programming, 99(2):283-296, 2004. Google Scholar
  20. Siegfried M Rump. Mathematically rigorous global optimization in floating-point arithmetic. Optimization Methods and Software, 33(4-6):771-798, 2018. Google Scholar
  21. Sriram Sankaranarayanan, Thao Dang, and Franjo Ivančić. Symbolic model checking of hybrid systems using template polyhedra. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 188-202. Springer, 2008. Google Scholar
  22. Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna. Scalable analysis of linear systems using mathematical programming. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 25-41. Springer, 2005. Google Scholar
  23. Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1998. Google Scholar
  24. Gagandeep Singh, Markus Püschel, and Martin T. Vechev. Making numerical program analysis fast. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 303-313. ACM, 2015. Google Scholar
  25. Gagandeep Singh, Markus Püschel, and Martin T. Vechev. A practical construction for decomposing numerical abstract domains. Proc. ACM Program. Lang., 2(POPL):55:1-55:28, 2018. Google Scholar
  26. H Paul Williams. Fourier’s method of linear programming and its dual. The American mathematical monthly, 93(9):681-695, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact