Laboratoire d'informatique de l'École polytechnique


Talk by Riccardo Gozzi: «Analog characterization of standard complexity classes by means of ODEs»

Speaker: Riccardo Gozzi
Location: Online
Date: Wed, 12 May 2021, 10:30-11:30

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Riccardo Gozzi.

Abstract: In this presentation it will be shown how to make use of ordinary differential equations (ODEs) to describe standard complexity classes. Previously it was shown that the classes P and FP can be characterized with ODEs. Here we show that ODEs can also be used to characterize a wide range of computable functions, from exponentials up to including all elementary functions. It will be also discussed the case of space complexity classes, introducing the definition of a particular dynamical system able to describe functions in FPSPACE. Finally, to complement what have been done with functions, the treatment of classes of languages such as EXPTIME and PSPACE will be included in the analysis.

Link to the online conference

Talk by Song Fei: «Spark-based Cloud Data Analytics using Multi-Objective Optimization»

Speaker: Song Fei
Location: Online
Date: Wed, 5 May 2021, 15:00-16:00

Song Fei will present his work on May 5th at 3pm.

It will be online

Abstract: Data analytics in the cloud has become an integral part of enterprise businesses. Big data analytics systems, however, still lack the ability to take task objectives such as user performance goals and budgetary constraints and automatically configure an analytic job to achieve these objectives. This paper presents UDAO, a Spark-based Unified Data Analytics Optimizer that can automatically determine a cluster configuration with a suitable number of cores as well as other system parameters that best meet the task objectives. At a core of our work is a principled multi-objective optimization (MOO) approach that computes a Pareto optimal set of configurations to reveal tradeoffs between different objectives, recommends a new Spark configuration that best explores such tradeoffs, and employs novel optimizations to enable such recommendations within a few seconds. Detailed experiments using benchmark workloads show that our MOO techniques provide a 2-50x speedup over existing MOO methods, while offering good coverage of the Pareto frontier. Compared to Ottertune, a state-of-the-art performance tuning system, UDAO recommends Spark configurations that yield 26%-49% reduction of running time of the TPCx-BB benchmark while adapting to different user preferences on multiple objectives.

Talk by Georg Struth: «Verifying Hybrid Systems with Interactive Theorem Provers»

Speaker: Georg Struth
Location: Online
Date: Wed, 21 Apr 2021, 11:00-12:00

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Georg Struth.

Link to the online conference

Abstract: Hybrid systems integrate continuous dynamics and discrete control. A prominent approach is differential dynamic logic (dL), a modal logic for reasoning about ordinary differential equations and their solutions within hybrid programs. Over the last decade, a domain-specific sequent calculus for dL has been developed together with an intricate explicit substitution calculus for it. It has been integrated into the KeYmaera X tool and proved its worth in numerous case studies.

This talk presents an algebraic reconstruction of this approach and the first verification and refinement components in an interactive proof assistant inspired by it. Our components are based on shallow embeddings in which the proof theory of dL is by and large replaced by semantic equational reasoning about orbits and trajectories of dynamical systems in combination with discrete state updates. We use algebras, in particular variants of Kleene algebras and predicate transformer algebras, for automatic verification condition generation. We currently support a component for reasoning with weakest liberal preconditions, a Hoare logic and a refinement calculus for hybrid programs.

These allow us to verify hybrid programs in various ways: starting from hybrid program specifications based on ordinary differential equations, we can certify solutions of locally Lipschitz-continuous vector fields using the Picard-Lindelöf theorem and then reason explicitly about them. Alternatively we can represent solutions of continuous vector fields implicitly by invariant sets. Finally, we can analyse hybrid program that specify trajectories or orbits of hybrid systems directly.

Apart from presenting the algebras used and their extension and instantiation to hybrid program semantics, I will present some examples, comment on the intricacies of formalising the approach within the Isabelle/HOL proof assistant, and outline some future directions for this line of work, time permitting.

This work is joint with Jonathan Julián Huerta y Munive, and partially funded by CONACYT.

The list of next seminars can be found at:

The calendar of seminars can be found at:

Factoring integers with oracles

Speaker: Francois Morain
Date: Thu, 15 Apr 2021, 13:00-14:15

The famous RSA cryptosystem is in danger if factoring integers is easy. In the classical world, factoring is considered difficult, contrary to the quantum world, where it can be done in polynomial time using Shor’s algorithm. Yet, no efficient implementation of this algorithm is known and we have some time to improve our understanding of the classical difficulty of factoring before this existed. One way to look at this is to add some knowledge (given as an oracle) about the factors we are looking for. Some of these can come from real bad generation of the primes used in RSA, for instance revealing some fraction of their bits. Other oracles are associated with arithmetic functions, such as Euler’s totient function. The aim of this talk is to give a survey of these oracles and give new results obtained with G. Renault and B. Smith.

Talk by Renaud Vilmart: « An introduction to ZX-calculus »

Speaker: Renaud Vilmart
Location: Online
Date: Wed, 14 Apr 2021, 11:00-12:00

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Renaud Vilmart for a tal entitled An introduction to ZX-calculus.

Abstract: The ZX-Calculus is a powerful graphical language for representing quantum processes, stemming from category theory. Its primitives are close to that of the hardware these processes will supposedly be implemented on, and yet it enjoys some level of abstraction. In particular, it is equipped with an intuitive equational theory, allowing us to relate processes that are equivalent, i.e. that represent the same quantum evolution. The plasticity and the equational theory of the language make it a particularly good candidate for unifying different models of quantum computation, for optimisation, as well as for verifying properties or equivalences of processes.

Link to the online conference

The list of next seminars can be found at:

The calendar of seminars can be found at:

Talk by Evelyne Hubert: «Sparse Interpolation in terms of multivariate Chebyshev polynomials»

Speaker: Evelyne Hubert
Location: Online
Date: Mon, 12 Apr 2021, 15:00-16:00

The next seminar of the MAX team will take place on Monday April 12 at 15:00 (note the unusual time). The speaker is Evelyne Hubert, she will speak about “Sparse Interpolation in terms of multivariate Chebyshev polynomials” (see the abstract below). The link is

Abstract: Sparse interpolation refers to the exact recovery of a function as a short linear combination of basis functions from a limited number of evaluations. For multivariate functions, the case of the monomial basis is well studied, as is now the basis of exponential functions. Beyond the multivariate Chebyshev polynomial obtained as tensor products of univariate Chebyshev polynomials, the theory of root systems allows to define a variety of generalized multivariate Chebyshev polynomials that have connections to topics such as Fourier analysis and representations of Lie algebras. We present a deterministic algorithm to recover a function that is the linear combination of at most r such polynomials from the knowledge of r and an explicitly bounded number of evaluations of this function.

This is a joint work with Michael Singer (