PPLite: zero-overhead encoding of NNC polyhedra. (English) Zbl 1496.68351
Summary: We present an alternative Double Description representation for the domain of NNC (not necessarily closed) polyhedra, together with the corresponding Chernikova-like conversion procedure. The representation uses no slack variable at all and provides a solution to a few technical issues caused by the encoding of an NNC polyhedron as a closed polyhedron in a higher dimension space. We then reconstruct the abstract domain of NNC polyhedra, providing all the operators needed to interface it with commonly available static analysis tools: while doing this, we highlight the efficiency gains enabled by the new representation and we show how the canonicity of the new representation allows for the specification of proper, semantic widening operators. A thorough experimental evaluation shows that our new abstract domain achieves significant efficiency improvements with respect to classical implementations for NNC polyhedra.
MSC:
| 68U05 | Computer graphics; computational geometry (digital and algorithmic aspects) |
| 52B55 | Computational aspects related to convexity |
References:
| [1] | Amato, G.; Scozzari, F.; Zaffanella, E., Efficient constraint/generator removal from double description of polyhedra, Electron. Notes Theor. Comput. Sci., 307, 3-15 (2014) · Zbl 1337.68262 |
| [2] | Assarf, B.; Gawrilow, E.; Herr, K.; Joswig, M.; Lorenz, B.; Paffenholz, A.; Rehn, T., Computing convex hulls and counting integer points with polymake, Math. Program. Comput., 9, 1-38 (2017) · Zbl 1370.90009 |
| [3] | Bagnara, R.; Hill, P. M.; Mazzi, E.; Zaffanella, E., Widening operators for weakly-relational numeric abstractions, (Hankin, C.; Siveroni, I., Static Analysis: Proceedings of the 12th International Symposium (2005), Springer-Verlag: Springer-Verlag Berlin, London, UK), 3-18 · Zbl 1141.68445 |
| [4] | Bagnara, R.; Hill, P. M.; Ricci, E.; Zaffanella, E., Precise widening operators for convex polyhedra, (Cousot, R., Static Analysis: Proceedings of the 10th International Symposium (2003), Springer-Verlag: Springer-Verlag Berlin, San Diego, California, USA), 337-354 · Zbl 1067.68578 |
| [5] | Bagnara, R.; Hill, P. M.; Ricci, E.; Zaffanella, E., Precise widening operators for convex polyhedra, Sci. Comput. Program., 58, 28-56 (2005) · Zbl 1088.68173 |
| [6] | Bagnara, R.; Hill, P. M.; Zaffanella, E., A new encoding of not necessarily closed convex polyhedra, (Carro, M.; Vacheret, C.; Lau, K. K., Proceedings of the 1st CoLogNet Workshop on Component-Based Software Development and Implementation Technology for Computational Logic Systems. Proceedings of the 1st CoLogNet Workshop on Component-Based Software Development and Implementation Technology for Computational Logic Systems, Madrid, Spain (2002), Universidad Politécnica de Madrid, Facultad de Informática), 147-153, Published as TR Number CLIP4/02.0 |
| [7] | Bagnara, R.; Hill, P. M.; Zaffanella, E., Widening operators for powerset domains, (Steffen, B.; Levi, G., Verification, Model Checking and Abstract Interpretation: Proceedings of the 5th International Conference. Verification, Model Checking and Abstract Interpretation: Proceedings of the 5th International Conference, VMCAI 2004 (2003), Springer-Verlag: Springer-Verlag Berlin, Venice, Italy), 135-148 · Zbl 1202.68242 |
| [8] | Bagnara, R.; Hill, P. M.; Zaffanella, E., Not necessarily closed convex polyhedra and the double description method, Form. Asp. Comput., 17, 222-257 (2005) · Zbl 1101.68674 |
| [9] | Bagnara, R.; Hill, P. M.; Zaffanella, E., Widening operators for powerset domains, Int. J. Softw. Tools Technol. Transf., 8, 449-466 (2006) |
| [10] | Bagnara, R.; Hill, P. M.; Zaffanella, E., The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program., 72, 3-21 (2008) |
| [11] | Bagnara, R.; Hill, P. M.; Zaffanella, E., Applications of polyhedral computations to the analysis and verification of hardware and software systems, Theor. Comput. Sci., 410, 4672-4691 (2009) · Zbl 1187.68311 |
| [12] | Bagnara, R.; Hill, P. M.; Zaffanella, E., Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness, Form. Methods Syst. Des., 35, 279-323 (2009) · Zbl 1185.68405 |
| [13] | Bagnara, R.; Ricci, E.; Zaffanella, E.; Hill, P. M., Possibly not closed convex polyhedra and the Parma Polyhedra Library, (Hermenegildo, M. V.; Puebla, G., Static Analysis: Proceedings of the 9th International Symposium (2002), Springer-Verlag: Springer-Verlag Berlin, Madrid, Spain), 213-229 · Zbl 1015.68215 |
| [14] | Bastoul, C., Code generation in the polyhedral model is easier than you think, (Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques (PACT 2004) (2004), IEEE Computer Society: IEEE Computer Society Antibes Juan-les-Pins, France), 7-16 |
| [15] | Becchi, A.; Zaffanella, E., A direct encoding for NNC polyhedra, (Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (2018)), 230-248 · Zbl 1511.68069 |
| [16] | Becchi, A.; Zaffanella, E., An efficient abstract domain for not necessarily closed polyhedra, (Podelski, A., Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings (2018), Springer), 146-165 · Zbl 1511.68070 |
| [17] | Becchi, A.; Zaffanella, E., Revisiting polyhedral analysis for hybrid systems, (Chang, B. E., Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings (2019), Springer), 183-202 · Zbl 1539.68149 |
| [18] | Benerecetti, M.; Faella, M.; Minopoli, S., Automatic synthesis of switching controllers for linear hybrid systems: safety control, Theor. Comput. Sci., 493, 116-138 (2013) · Zbl 1294.93041 |
| [19] | Birkhoff, G., Lattice Theory. Volume XXV of Colloquium Publications (1967), American Mathematical Society: American Mathematical Society Providence, Rhode Island, USA · Zbl 0153.02501 |
| [20] | Chernikova, N. V., Algorithm for finding a general formula for the non-negative solutions of system of linear equations, USSR Comput. Math. Math. Phys., 4, 151-158 (1964) · Zbl 0221.65055 |
| [21] | Chernikova, N. V., Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities, USSR Comput. Math. Math. Phys., 5, 228-233 (1965) · Zbl 0171.35701 |
| [22] | Chernikova, N. V., Algorithm for discovering the set of all solutions of a linear programming problem, USSR Comput. Math. Math. Phys., 8, 282-293 (1968) · Zbl 0218.90030 |
| [23] | Colón, M. A.; Sipma, H. B., Synthesis of linear ranking functions, (Margaria, T.; Yi, W., Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference. Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001 (2001), Springer-Verlag: Springer-Verlag Berlin, Genova, Italy), 67-81 · Zbl 0978.68095 |
| [24] | Cortesi, A., Widening operators for abstract interpretation, (Sixth IEEE International Conference on Software Engineering and Formal Methods. Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, South Africa (2008)), 31-40 |
| [25] | Cortesi, A.; Zanioli, M., Widening and narrowing operators for abstract interpretation, Comput. Lang. Syst. Struct., 37, 24-42 (2011) · Zbl 1218.68100 |
| [26] | Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages (1977), ACM Press: ACM Press Los Angeles, CA, USA), 238-252 |
| [27] | Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages (1979), ACM Press: ACM Press San Antonio, TX, USA), 269-282 |
| [28] | Cousot, P.; Cousot, R., Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, (Bruynooghe, M.; Wirsing, M., Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (1992), Springer-Verlag: Springer-Verlag Berlin, Leuven, Belgium), 269-295 |
| [29] | Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (1978), ACM Press: ACM Press Tucson, Arizona), 84-96 |
| [30] | Doose, D.; Mammeri, Z., Polyhedra-based approach for incremental validation of real-time systems, (Yang, L. T.; Amamiya, M.; Liu, Z.; Guo, M.; Rammig, F. J., Proceedings of the International Conference on Embedded and Ubiquitous Computing. Proceedings of the International Conference on Embedded and Ubiquitous Computing, EUC 2005 (2005), Springer-Verlag: Springer-Verlag Berlin, Nagasaki, Japan), 184-193 |
| [31] | Ellenbogen, R., Fully Automatic Verification of Absence of Errors via Interprocedural Integer Analysis (2004), School of Computer Science, Tel-Aviv University: School of Computer Science, Tel-Aviv University Tel-Aviv, Israel, Master’s thesis |
| [32] | Fehnker, A.; Ivancic, F., Benchmarks for hybrid systems verification, (Alur, R.; Pappas, G., Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004 (2004), Proceedings, Springer), 326-341 · Zbl 1135.93324 |
| [33] | Frehse, G., PHAVer: algorithmic verification of hybrid systems past HyTech, Int. J. Softw. Tools Technol. Transf., 10, 263-279 (2008) |
| [34] | Frehse, G.; Abate, A.; Adzkiya, D.; Becchi, A.; Bu, L.; Cimatti, A.; Giacobbe, M.; Griggio, A.; Mover, S.; Mufid, M.; Riouak, I.; Tonetta, S.; Zaffanella, E., ARCH-COMP19 category report: hybrid systems with piecewise constant dynamics, (Frehse, G.; Althoff, M., ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EasyChair (2019)), 1-13 |
| [35] | Fukuda, K.; Prodon, A., Double description method revisited, (Deza, M.; Euler, R.; Manoussakis, Y., Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5, 1995, Selected Papers (1996), Springer-Verlag: Springer-Verlag Berlin), 91-111 · Zbl 1543.68253 |
| [36] | Genov, B., The Convex Hull Problem in Practice: Improving the Running Time of the Double Description Method (2014), University of Bremen: University of Bremen Germany, Ph.D. thesis |
| [37] | Gopan, D., Numeric Program Analysis Techniques with Applications to Array Analysis and Library Summarization (2007), University of Wisconsin: University of Wisconsin Madison, Wisconsin, USA, Ph.D. thesis |
| [38] | Halbwachs, N., Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme (1979), Université scientifique et médicale de Grenoble: Université scientifique et médicale de Grenoble Grenoble, France, Thèse de 3^ème cycle d’informatique |
| [39] | Halbwachs, N.; Proy, Y. E.; Raymond, P., Verification of linear hybrid systems by means of convex approximations, (Le Charlier, B., Static Analysis: Proceedings of the 1st International Symposium (1994), Springer-Verlag: Springer-Verlag Berlin, Namur, Belgium), 223-237 |
| [40] | Halbwachs, N.; Proy, Y. E.; Roumanoff, P., Verification of real-time systems using linear relation analysis, Form. Methods Syst. Des., 11, 157-185 (1997) |
| [41] | Henry, J.; Monniaux, D.; Moy, M., PAGAI: a path sensitive static analyser, Electron. Notes Theor. Comput. Sci., 289, 15-25 (2012) |
| [42] | Jeannet, B.; Miné, A., Apron: a library of numerical abstract domains for static analysis, (Bouajjani, A.; Maler, O., Computer Aided Verification, Proceedings of the 21st International Conference. Computer Aided Verification, Proceedings of the 21st International Conference, CAV 2009 (2009), Springer: Springer Grenoble, France), 661-667 |
| [43] | Kaibel, V.; Pfetsch, M. E., Computing the face lattice of a polytope from its vertex-facet incidences, Comput. Geom., 23, 281-290 (2002) · Zbl 1015.52010 |
| [44] | Le Verge, H., A Note on Chernikova’s Algorithm (1992), IRISA: IRISA Campus de Beaulieu, Rennes, France, Publication Interne 635 |
| [45] | Miné, A., Weakly Relational Numerical Abstract Domains (2005), École Polytechnique: École Polytechnique Paris, France, Ph.D. thesis |
| [46] | Motzkin, T. S.; Raiffa, H.; Thompson, G. L.; Thrall, R. M., The double description method, (Kuhn, H. W.; Tucker, A. W., Contributions to the Theory of Games - Volume II. Contributions to the Theory of Games - Volume II, Annals of Mathematics Studies, vol. 28 (1953), Princeton University Press: Princeton University Press Princeton, New Jersey), 51-73 · Zbl 0050.14201 |
| [47] | Notani, V.; Giacobazzi, R., Learning based widening, (Contribution to the 8th Workshop on Tools for Automatic Program Analysis. Contribution to the 8th Workshop on Tools for Automatic Program Analysis, TAPAS’17, New York (2017)) |
| [48] | Perri, S., Un algoritmo stile Chernikova per poliedri NNC (A Chernikova-style Algorithm for NNC Polyhedra) (2012), Department of Mathematics and Computer Science, University of Parma: Department of Mathematics and Computer Science, University of Parma Italy, in Italian |
| [49] | Pop, S.; Silber, G. A.; Cohen, A.; Bastoul, C.; Girbal, S.; Vasilache, N., GRAPHITE: Polyhedral Analyses and Optimizations for GCC (2006), Centre de Recherche en Informatique, École des Mines de Paris: Centre de Recherche en Informatique, École des Mines de Paris Fontainebleau, France, Contribution to the GNU Compilers Collection Developers Summit 2006 (GCC Summit 06), Ottawa, Canada, June 28-30, 2006 |
| [50] | Singh, G.; Püschel, M.; Vechev, M. T., Fast polyhedra abstract domain, (Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 (2017)), 46-59 · Zbl 1380.68131 |
| [51] | Stoer, J.; Witzgall, C., Convexity and Optimization in Finite Dimensions I (1970), Springer-Verlag: Springer-Verlag Berlin · Zbl 0203.52203 |
| [52] | 4ti2—a software package for algebraic, geometric and combinatorial problems on linear spaces (2018), Available at |
| [53] | Terzer, M.; Stelling, J., Large-scale computation of elementary flux modes with bit pattern trees, Bioinformatics, 24, 2229-2235 (2008) |
| [54] | Terzer, M.; Stelling, J., Parallel extreme ray and pathway computation, (Parallel Processing and Applied Mathematics, 8th International Conference. Parallel Processing and Applied Mathematics, 8th International Conference, PPAM 2009, Wroclaw, Poland, 2009 (2009)), 300-309, Revised Selected Papers, Part II |
| [55] | Zaffanella, E., On the efficiency of convex polyhedra, Electron. Notes Theor. Comput. Sci., 334, 31-44 (2018) · Zbl 1525.68032 |
| [56] | Zolotykh, N. Y., New modification of the double description method for constructing the skeleton of a polyhedral cone, Comput. Math. Math. Phys., 52, 146-156 (2012) · Zbl 1249.52017 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
