Section: Highlights of the Year

Highlights of the Year

Performance evaluation of the 17-18-112 call center in Paris

Vianney Bœuf completed his PhD, done in collaboration with Brigade des Sapeurs Pompiers de Paris, on the performance evaluation of the new organization of the Paris emergency call center developed by Préfecture de Police. See Section 7.5.2.

Maximal upper bounds in Löwner order

A classical theorem of Kadison (1951) shows that the set of real quadratic forms, equipped with the pointwise order, is an antilattice, meaning that two quadratic forms have a least upper bound (or dually, a greatest lower bound) if and only if they are comparable. In [23], Nikolas Stott gave a quantitative version of Kadison theorem, characterizing the set of minimal upper bound as the quotient an indefinite orthogonal group. Applications of these ideas to hybrid systems verification appeared in [16], [30].

Formal proofs in linear programming

Xavier Allamigeon and Ricardo Katz have formalized in the proof assistant Coq several basic results in the theory of convex polyhedra and linear optimization. These include Farkas Lemma, the duality theorem of linear programming, separation from convex hulls, Minkowski Theorem, etc. See [27] and Section 7.3.1.