We introduce a new numerical abstract domain able to infer min and max invariants over the program variables, based on max-plus polyhedra. Our abstraction is more precise than octagons, and allows to express non-convex properties without any disjunctive representations. We have defined sound abstract operators, evaluated their complexity, and implemented them in a static analyzer. It is able to automatically compute precise properties on numerical and memory manipulating programs such as algorithms on strings and arrays. © 2008 Springer-Verlag.
CITATION STYLE
Allamigeon, X., Gaubert, S., & Goubault, É. (2008). Inferring min and max invariants using max-plus polyhedra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5079 LNCS, pp. 189–204). https://doi.org/10.1007/978-3-540-69166-2_13
Mendeley helps you to discover research relevant for your work.