Joint work with Salomon Sickert

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of LTL with past operators is equivalent to a formula of the form $\bigwedge_{i=1}^n \G\F \varphi_i \vee \F\G \psi_i $, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for the future fragment of LTL. Both normalisation procedures had a non-elementary worst-case blow-up, and followed an involved path from LTL formulas to counter-free automata to star-free regular expressions and back to LTL. We improve on both points. We present a purely syntactic normalisation procedure from LTL to LTL, with single exponential blow-up, that can be implemented in a few dozen lines of Standard ML code. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

We present new classical and quantum algorithms for solving random hard instances of the subset-sum problem, in which we are given n integers on n bits and try to find a subset of them that sums to a given target. This classical NP-complete problem has several applications in cryptography and underlies the security of some proposed post-quantum cryptosystems. At EUROCRYPT 2010, Howgrave-Graham and Joux (HGJ) introduced the representation technique and presented an algorithm running in time $\tilde{O}(2^{0.337 n})$. This asymptotic time was improved by Becker, Coron, Joux (BCJ) at EUROCRYPT 2011. We show how to improve this further. We then move to the context of quantum algorithms. The two previous quantum speedups in the literature are given by Bernstein, Jeffery, Lange and Meurer (PQCRYPTO 2013) and Helm and May (TQC 2018), which are respectively quantum versions of HGJ and BCJ. They both rely on the framework of quantum walks, use exponential quantum memory with quantum random-access and require an unproven conjecture on quantum walk updates. We devise a new algorithm, using quantum search only, that achieves the first quantum speedup in the model of classical memory with quantum random access. Next, we study improvements for the quantum walks. We show how to avoid the quantum walk conjecture and give a better quantum walk time complexity for subset-sum.

Joint work with Xavier Bonnetain and Rémi Bricout.

The closeness centrality measure associates to each node of a graph its average distance from all the other nodes. In this talk, we will consider a temporal version of this measure, which have been recently introduced and analysed in the case of temporal graphs (that is, graphs in which edges can appear and disappear during time). In particular, we will show how this measure can be efficiently approximated by using a “backward” temporal breadth-first search algorithm and a classical sampling technique. We will then introduce a “temporally global” closeness centrality measure of a node in a temporal graph, which is quite similar to the notion of AUC (Area Under Curve), and we will show how this global measure can also be efficiently approximated. We conclude by presenting several experimental results in the case of medium/large real-world temporal networks. This is a joint work with Clémence Magnien and Andrea Marino.

Solidity is the dominant programming language for smart contracts on the Ethereum blockchain. This talk presents a high-level formalization of the Solidity language with a focus on the memory model. The memory model of Solidity has various unusual and non-trivial behaviors, providing a fertile ground for potential bugs. Smart contracts have access to two classes of data storage: a permanent storage that is a part of the global blockchain state, and a transient local memory used when executing transactions. While the local memory uses a standard heap of entities with references, the permanent storage has pure value semantics (although pointers to storage can be declared locally). This memory model that combines both value and reference semantics - with all interactions between the two - poses some interesting challenges but also offers great opportunities for automation. The presented formalization covers all features of the language related to managing state and memory in an effective way: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify tool and we provide an evaluation on an extensive test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.

Nous présentons une involution sur les intervalles de Tamari qui échange deux séries de statistiques : les “montées” et les “contacts”. Cette involution fait intervenir de nombreux objets combinatoires : chemins de Dyck, arbres, intervalles-posets.