Selfie is a self-contained 64-bit, 10-KLOC implementation of (1) a self-compiling compiler written in a tiny subset of C called C* targeting a tiny subset of 64-bit RISC-V called RISC-U, (2) a self-executing RISC-U emulator, (3) a self-hosting hypervisor that virtualizes the emulated RISC-U machine, and (4) a prototypical symbolic execution engine that executes RISC-U symbolically. Selfie can compile, execute, and virtualize itself any number of times in a single invocation of the system given adequate resources. There is also a simple linker, disassembler, debugger, and profiler. C* supports only two data types, uint64_t and uint64_t*, and RISC-U features just 14 instructions, in particular for unsigned arithmetic only, which significantly simplifies reasoning about correctness. Selfie has originally been developed just for educational purposes but has by now become a research platform as well. We discuss how selfie leverages the synergy of integrating compiler, target machine, and hypervisor in one self-referential package while orthogonalizing bootstrapping, virtual and heap memory management, emulated and virtualized concurrency, and even replay debugging and symbolic execution.

This is joint work with Alireza S. Abyaneh, Simon Bauer, Philipp Mayer, Christian Mösl, Clément Poncelet, Sara Seidl, Ana Sokolova, and Manuel Widmoser, University of Salzburg, Austria.

Web: http://selfie.cs.uni-salzburg.at

A generalized lexicographical order on infinite words is defined by choosing for each position a total order on the alphabet. This allows to define generalized Lyndon words. Every word in the free monoid can be factorized in a unique way as a non-increasing factorization of generalized Lyndon words. We give new characterizations of the first and the last factor in this factorization as well as new characterization of generalized Lyndon words. We also give more specific results on two special cases: the classical one and the one arising from the alternating lexicographical order. This is a joint work with Antonio Restivo and Christophe Reutenauer.

It is well known that there is a connection between resolution complexity of a formula and complexity of (very weak) branching programs for the corresponding search problem. In the talk, we will discuss proof systems that allow to generalize this statement and explain the lower bounds for these proof systems. In order to achieve this lower bounds, we show how to transform functions with a high fixed-partition communication complexity into functions with a high best-partition communication complexity and as a result, we translate the landscape of fixed-partition communication complexity classes into the landscape of best-partition communication complexity classes.

In the literature, two kinds of process crashes are usually considered: initially dead processes and “classical” crash failures (that can occur at any time). A new notion of process failure explicitly related to contention has recently been introduced by Gadi Taubenfeld (NETYS 2018). More precisely, given a predefined contention threshold λ, this notion considers the execution in which process crashes are restricted to occur only when process contention is smaller than or equal to λ. If crashes occur after contention bypassed λ, there are no correctness guarantees. It was shown that, when λ = n-1, consensus can be solved in an n-process asynchronous read/write system despite the crash of one process, thereby circumventing the well-known FLP impossibility result.

In this talk, I will present k-set agreement and renaming algorithms that are resilient to two types of process crash failures: “λ-constrained” crash failures (as previously defined) and classical crash failures.

Le parallélisme synchrone est utilisé aujourd'hui de manière routinière pour concevoir et implémenter le logiciel de controle/commande critique, dans les avions ou les train, par exemple. Il permet d'écrire un modèle mathématique idéal du système en faisant l'hypothèse que tous les processus partagent une échelle de temps globale commune. On raisonne d'abord en négligeant les temps de calculs et de communication, ce qui simplifie la détection de certaines erreurs (interblocages, courses critiques) et les étapes de validation (simulation, test, vérification formelle). Puis on vérifie que le code généré par le compilateur respecte les contraintes de temps d'exécution pire-cas.

Les langages synchrones décrivent des systèmes à temps discret seulement. Ils ne permettent pas de modéliser, ni fidèlement ni très efficacement des systèmes contenant des dynamiques hybrides combinant des signaux à temps discret et à temps continu. Cela créé une rupture dans la chaîne de développement, avec un langage pour la modélisation hybride et un autre pour la modélisation ou l'implémementation du logiciel de contrôle.

Dans cet exposé, nous présenterons Zelus, une extension d'un langage synchrone avec des équations différentielles ordinaires (ODEs) et une opération de détection d'événement (zero-crossing). Il permet d'écrire dans un source unique, un modèle synchrone (à temps discret) du logiciel de controle et un modèle (à temps discret où à temps continu) de son environnement. Nous illustrerons le langage sur quelques exemples. Nous présenterons son système de types qui permet de cloisonner les parties à temps discret et les parties à temps continu pour rejeter des comportements étranges que l'on obtient avec les outils de modélisation hybrides les plus utilisés. Nous montrerons également son analyse par typage des boucles de causalité par typage. Enfin, nous montrerons le principe utilisé pour générer du code séquentiel qui est lié ensuite à un solveur numérique (ici Sundials Cvode). Si le temps le permet, nous discuterons une expérimentation en cours, d'ajout de contructions de programmes probabilistes, ainsi que quelques questions ouvertes autour du typage, de la sémantique et de la vérification.

In this talk we consider non-stochastic versions of the games introduced in the first lecture, namely Mean Payoff Games (MPGs) and Energy Games (EGs). We show reductions between these two games. We then describe a pseudo-polynomial time algorithm of Brim et al. for EGs, and hence also MPGs

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Dans le contexte des réseaux à grande échelle, la prise en compte des pannes est une nécessité. L’auto-stabilisation est une approche algorithmique de la tolérance aux pannes dans les systèmes distribués dont le but est de gérer la corruption de la mémoire des processeurs dues à des pannes transitoires. Plusieurs paramètres caractérisent l’efficacité d’un algorithme auto-stabilisant, dont en particulier (1) le temps pris par le système pour retourner dans une configuration légale suite à une corruption arbitraire de la mémoire de ses processeurs, et (2) l’espace mémoire utilisé par les processeurs pour exécuter l’algorithme. La minimisation de l'espace mémoire est motivée pas de nombreux aspects : existence de réseaux (tels que les réseaux de capteurs) offrant des espaces mémoires limités, la minimisation des échanges de données entre processeurs voisins, la limitation du stockage d’information afin de pouvoir utiliser des techniques de redondance, etc. Ce séminaire présentera l’auto-stabilisation au travers deux grands problèmes classiques : la construction d’arbres couvrants, notamment d’arbres couvrants de poids minimum, et l’election d'un leader. Il présentera en particulier les liens entre auto-stabilisation et les techniques de décision distribuée, incluant le calcul de bornes inférieures sur l’espace mémoire nécessaire à la résolution par des algorithmes auto-stabilisants des problèmes susmentionnés.

Taylor expansions have been introduced by Ehrhard and Regnier as a computational interpretation of Girard's quantitative semantics. Lambda-terms are expanded into linear combinations of their n-linear approximants, such approximants being defined as resource lambda-terms. This construction is well-suited to interpret quantitative calculi, such as the probabilistic lambda-calculus: Taylor expansions are linear combinations and the resource lambda-calculus is linear so interpreting probability distributions over terms is straightforward. Yet paradoxically the proof technique used by Ehrhard and Regnier to study Taylor expansions heavily rely on the particular structure of the expansions of ordinary lambda terms, and they are not suited to work on a quantitative setting. In this talk we will show how to indirectly extend their result to probabilistic Taylor expansions. First we will introduce explicit Taylor expansions, which uses “inert” probabilistic choices to interpret probabilistic terms while preserving the necessary properties to apply Ehrhard and Regnier's proof techniques. Then we will show how to extract interesting results on probabilistic Taylor expansions from these explicit Taylor expansions.

I will review some of my previous results on code transformations. Everybody knows refactoring that have been widespread by Martin Fowler at the end of the 1990s. A refactoring is a transformation, preserving the behavior of the software system. Such transformations have also the properties to be performed daily and to affect very few entities. At the opposite of the spectrum, there is architecture evolutions that occur once or twice in the software system lifecycle and involve almost the whole system. In between there are a large space for transformations frequently performed almost like refactoring but may impact the behavior. We present two contexts where we applied such transformations.

Anonymity is a primary ingredient for our digital life. Several tools have been designed to address it, namely blind signatures, group signatures or anonymous credentials for authentication and randomizable encryption or mix-nets, for confidentiality. When it comes to complex electronic voting schemes, random shuffling of ciphertexts with mix-nets is the only known tool and has been largely used in practice, for example in the recent professional election of National Education with more than 430 000 votes. However, achieving anonymity requires huge and complex zero-knowledge proofs to guarantee the actual permutation of the initial ciphertexts.

In this talk, we propose a new approach for proving correct shuffling based on the new notion of extractable linearly-homomorphic signature: the mix-servers can simply randomize individual ballots (meaning the ciphertexts, the signatures, and the verification keys) with an additional global proof of constant size, and the output will be publicly verifiable. The computational complexity for the mix-servers is linear in the number of ciphertexts. It also remains linear in the number of ciphertexts for the verifiers, independently of the number of rounds of mixing. This leads to the most efficient technique of mix-nets, which is at the same time highly scalable.

(Joint work with Hebant Chloé and David Pointcheval)