Project topics and materials
Get Complete Project Material File(s) Now! »
Preliminaries on tropical algebra
Tropical algebra usually refers to the min-plus semiring, which is the set R ∪ {+∞} where the addition of two elements x and y is defined as min(x, y), and the multiplication as the classical addition x + y. However, in this manuscript, we will use the instantiation by the max-plus semiring, i.e. the set Rmax def = R∪ {−∞} endowed with the additive law ⊕ defined as x ⊕ y def = max(x, y), and the multiplicative law ⊗ defined as x ⊗ y def = x + y. Observe that this formulation is totally equivalent since the max-plus and min-plus semirings are in one-to-one correspondence by the function x 7→ −x (with the convention that −∞ is mapped to +∞).
Other instantiations of tropical algebra could also be used (see [Pin98] for a survey on tropical semirings). For instance, we could consider the semiring R+ of positive reals, equipped with max and × as additive and multiplicative laws. Besides, the max-plus semiring of integers (Z ∪ {−∞},⊕,⊗) is of particular interest for applications to computer science. Indeed, it can be implemented with multi-precision integers, and does not raise the critical question of the representation of reals by floating-point numbers (see [Mon08]). Similarly, booleans { 0, 1 } form a semiring, equipped with the disjunction as addition, and the conjunction as multiplication. Semirings are defined similarly to rings, but their elements do not necessarily have an inverse with respect to the additive law: Definition 2.1. A set S equipped with the binary operations ⊕ and ⊗ is a semiring if the following requirements are satisfied:
❼ (S,⊕) is a commutative monoid equipped with a zero element ✵,
❼ (S,⊗) is a monoid provided with a unit element ✶,
❼ the multiplication is distributive over the addition, i.e. for all x, y, z ∈ S,
Characterizing extremality using directed hypergraphs
We are now going to show how the combinatorial extremality criterion based on the { ✵, ✶ }- elements of the tangent cone can be expressed using directed hypergraphs.
Directed hypergraphs and related notions are introduced in Section 3.3.1. Directed hypergraphs are a generalization of directed graphs, just as hypergraphs for graphs. In Section 3.3.2, we introduce the notion of tangent directed hypergraph, which is an equivalent encoding of the tangent cone as a hypergraph. Corollary 3.11 is then rewritten in terms of the reachability relation of the tangent hypergraph. Theorem 3.3 proves that the extremality reduces to the existence of a particular strongly connected component playing the role of a sink.
Computing maximal strongly connected components
In this section, we describe an algorithm which determines the maximal Sccs for the order in directed hypergraphs. In particular, it returns the number of such Sccs.3 Its principle is discussed in Section 4.2.1. We provide a first and suboptimal sketch of the algorithm. The key idea is that maximal Sccs in a directed hypergraph can be computed by an alternative sequence of operations of two kinds: (i) merging some nodes in the directed hypergraph, (ii) discovering the maximal Sccs in an underlying directed graph. For this reason, we define in Section 4.2.2 a variation of Tarjan’s algorithm which determines the maximal Sccs of a directed graph in linear time. Finally, in Section 4.2.3, we build an optimized version of the sketch of the algorithm of Section 4.2.1, which executes in quasi-linear time. It relies on a particular instrumentation of hyperedges, which is quite technical. That is why we recommend that the reader make use of the execution trace given in Section 4.2.4.
Table of contents :
1 Introduction
1.1 Context of this work
1.2 Analyzing memory manipulations by abstract interpretation
1.2.1 Main principles of abstract interpretation
1.2.2 Abstractions for memory manipulations
1.3 An overview of tropical polyhedra
1.4 Contributions
1.5 Organization of the manuscript
1.6 A few words on notations
I Combinatorial and algorithmic aspects of tropical polyhedra
2 Introduction to tropical convexity
2.1 Preliminaries on tropical algebra
2.2 Preliminaries on tropical convexity
2.2.1 Notations
2.2.2 Tropical convex sets
2.2.3 Tropical cones
2.2.4 Extreme elements
2.2.5 Minimal generating representations
2.2.6 Tropical homogenization
2.3 Tropical polyhedra and polyhedral cones
2.3.1 Definition
2.3.2 Minkowski-Weyl theorem
2.3.3 Homogenization of tropical polyhedra
2.4 Conclusion of the chapter
3 Combinatorial characterization of extremality from halfspaces
3.1 Preliminaries on extremality
3.2 Characterizing extremality using the tangent cone
3.2.1 Tangent cone
3.2.2 The { ✵, ✶ }-cones and their extreme elements
3.3 Characterizing extremality using directed hypergraphs
3.3.1 Preliminaries on directed hypergraphs
3.3.2 Tangent directed hypergraph
3.4 Conclusion of the chapter
4 Maximal strongly connected components in directed hypergraphs
4.1 Reachability in directed hypergraphs
4.2 Computing maximal strongly connected components
4.2.1 Principle of the algorithm for directed hypergraphs
4.2.2 Computing maximal strongly connected components in directed graphs
4.2.3 Optimized algorithm
4.2.4 Example of a complete execution trace
4.3 Conclusion of the chapter
4.4 Proving Theorem 4.1
4.4.1 Correctness of the algorithm
4.4.2 Complexity proof
5 Algorithmics of tropical polyhedra
5.1 From the external description to the internal description
5.1.1 The tropical double description method
5.1.2 Resulting algorithm
5.1.3 Comparison with the existing approaches
5.1.4 Comparison with the classical double description method
5.1.5 Benchmarks
5.2 From the internal description to the external description
5.2.1 Polar of tropical cones
5.2.2 Polar of finitely generated cones
5.2.3 Efficient characterization of extreme elements of the polar of a polyhedraln cone
5.2.4 Resulting algorithm
5.2.5 Comparison with alternative approaches
5.3 The number of extreme elements in tropical polyhedra
5.3.1 A first McMullen-type bound
5.3.2 Signed cyclic polyhedral cones
5.3.3 Comparison with the classical case
5.3.4 The number of extreme rays in signed cyclic polyhedral cones
5.3.5 The number of extreme rays in polar cones
5.4 Conclusion of the chapter
II Application to static analysis by abstract interpretation
6 Introduction to static analysis by abstract interpretation
6.1 Kernel language
6.1.1 Principles of the language
6.1.2 Syntax of the language
6.2 Semantics of the language
6.2.1 Control-flow graph
6.2.2 Memory model
6.2.3 Operational semantics
6.2.4 Collecting semantics of a program
6.2.5 Proving the absence of heap overflows
6.3 Abstract interpretation
6.3.1 Theoretical framework
6.3.2 Numerical abstract domains
6.4 A first possible abstract semantics
6.5 An abstraction on strings
6.6 Conclusion of the chapt
7 Numerical abstract domains based on tropical polyhedra
7.1 Inferring max-invariants: the abstract domain MaxPoly
7.1.1 Definition of the abstract domain
7.1.2 Abstract preorder
7.1.3 Abstract union operator
7.1.4 Abstract intersection primitives
7.1.5 Abstract assignment operators
7.1.6 Widening operators
7.1.7 Reduction with zones
7.1.8 Non-tropically affine abstract primitives
7.1.9 Summary of abstract primitives behavior
7.2 Inferring min-invariants: the abstract domain MinPoly
7.2.1 Order-theoretic abstract primitives
7.2.2 Conditions and assignments
7.2.3 Reduction with zones
7.3 Inferring min- and max-invariants: the domain MinMaxPoly
7.3.1 Order-theoretic abstract primitives
7.3.2 Conditions and assignments
7.3.3 Reduction with octagons
7.4 Experiments
7.4.1 Principles of the implementation
7.4.2 Analysis of memory manipulating programs
7.4.3 Application to array predicate abstractions
7.4.4 Efficiently handling many disjunctions
7.4.5 Sort algorithms
7.4.6 Performance of the analysis
7.5 Conclusion of the chapter
8 Conclusion
8.1 Summary of the contributions
8.2 Perspectives
8.2.1 Combinatorics and algorithmics of tropical convex sets
8.2.2 Numerical abstract domains.
Bibliography
