Dans de nombreux écosystèmes de langages de programmation, les développeurs dépendent de plus en plus de dépendances externes en open source, disponibles via des gestionnaires de paquets. Les paquets clés qui ne sont pas maintenus présentent un risque pour les projets qui en dépendent ainsi que pour les écosystèmes. Par conséquent, des initiatives communautaires peuvent émerger au sein des écosystèmes pour résoudre ce problème en adoptant les paquets clés ayant des problèmes de maintenance. Dans mon exposé, je présenterai les résultats de l'article coécrit avec Jean-Rémy Falleri et récemment publié dans Empirical Software Engineering intitulé “A Grounded Theory of Community Package Maintenance Organizations”. Le but de celui-ci était de construire une théorie de ces organisations (CPMO), notamment leur émergence et leur mode de fonctionnement. Pour ce faire, nous avons utilisé une méthodologie qualitative appelée Grounded Theory. Nous avons analysé des documents existants provenant de plusieurs CPMO, tels que des documentations et des discussions sur des forums publics, complétés par des entretiens avec des initiateurs de CPMO. Je parlerai également de mon application de ce modèle d'organisation à l'écosystème Coq, avec la création de l'organisation Coq-community, et de l'expérience acquise par ce biais.

Memory management is notoriously difficult in a concurrent setting. The presence of garbage collection greatly simplifies the life of the programmer, eradicating many memory-related bugs. However, the heap space usage of garbage-collected programs can be tricky to understand and reason about, as there is no explicit program point where space is reclaimed.

We recently presented a Separation Logic with Space Credits to reason about heap space under garbage collection in a high-level, yet sequential, language.

In this talk, we scale up to a concurrent language. For this purpose, we introduce new “pointed-by-thread” assertions, which keep track of the existence of stack-to-heap pointers in a reasonably lightweight manner. We illustrate our approach on a range of examples, including the standard lock-free Treiber's stack, and unveil its surprisingly high heap memory bounds in the presence of garbage collection.

PureCake, is a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. This talk will present how optimization soundness can be proven using equational reasoning with the example of the demand analysis pass and other related optimizations.

Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

“Smart contract” are software whose byte code is executed by node validators/block makers operating a block chain. These “open^2” code (open source + open execution layer) provide an entirely transparent execution stack (on public blockchains) that is foreseen to complement (or even replace) most standard trusted third party based transactions (i.e based on trusting a bank, or a notary for settlement) in a near future.

In this workgroup I will introduce basic concepts of the Ethereum Virtual Machine (EVM) and Solidity (the most used programming language on top of the EVM). To illustrate these concepts I will describe Mangrove, a decentralised exchange protocol designed for the EVM. This should allow us to discuss difficulties and technical solutions that naturally arise when designing smart contracts managing user funds. In particular we will discuss current limitations of solidity and the need for better programming paradigms for critical onchain softwares.

Depuis 2013, le PAMAL (Preservation & Art – Media Archaeology Lab), qui devient en 2019 le PAMAL_Group, associe création et recherche dans le champ de l’archéologie des média. PAMAL_Group crée ses propres œuvres à partir d’œuvres d’art numérique disparues ou fortement endommagées en raison de l’obsolescence des logiciels et matériels informatiques. Ses travaux cherchent à rendre sensible la vulnérabilité d’un art fortement dépendant des logiques industrielles. Toutes les œuvres que le collectif reconstruit sont au plus près des matérialités d’origine. Le 13 avril, les deux membres fondateurs du PAMAL_Group viendront présenter les derniers projets télématiques du collectif, récemment exposés au Centre Pompidou et au ZKM (Zentrum für Kunst und Medien de Karlsruhe).

Dans cet exposé très informel à propos d'un travail en cours, je souhaiterais discuter de différents styles pour définir (en Coq) la sémantique d'un langage de programmation. Une de mes motivations est d'obtenir une sémantique au moins partiellement exécutable dans Coq et d'en tirer un mécanisme d'exécution symbolique qui pourrait être exploité dans un système de vérification de programmes.

Au cours de l'exposé, je présenterai deux styles de sémantique (pour un langage sans effets de bord, hormis divergence et plantage), et au-dessus de chacun d'eux, je construirai une logique de Hoare. Le premier style, “monadique jusqu'au bout”, reproduit des idées que l'on trouve dans la littérature: un premier interprète est exprimé dans une monade libre bien choisie, puis, dans un second temps, les habitants de cette monade sont traduits dans d'autres monades (monade des interaction trees; monade de spécification). Le second style, “à pas amples”, est hybride: dans une couche inférieure, on conserve le même interprète monadique, exprimé dans la monade libre; dans une couche supérieure, on raisonne à l'aide d'une sémantique opérationnelle à petits pas. J'aimerais recevoir des commentaires et suggestions du public afin de prévoir les prochaines étapes: ajout du non-déterminisme, du parallélisme, de l'état mutable, puis construction d'une logique de programmes de la famille Iris.

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This poses important safety, privacy, and non-discrimination challenges. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is mainly carried out in the ML community, while research in ML verification is mostly carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by presenting our recent and ongoing work on interpretability-aware verification of ML software. On the one hand, we show how verification can aid interpretability by providing a new feature importance measure for support vector machines. On the other hand, we discuss how interpretability can guide verification by proposing a new saliency-guided robustness verification problem for deep neural networks. We conclude with plans and perspectives on future work.

https://www.irill.org/events/2023/event20230202.html

Assembling off-the-shelf or independently-developed components into a system is a common practice. Although a few useful tools exist, this remains manual, ad-hoc, complex, labour-intensive, and error-prone.

Varda provides a higher level of abstraction. An Varda program describes how to compose components into a safe architecture. The programmer isolates an off-the-shelf (OTS) component behind an Varda shield, which specifies its interface, its protocol, and its pre- and post-conditions.

Components can be logically nested, providing encapsulation boundaries; the outer component orchestrates its inner components. It can intercept communication, as a general mechanism to compute over components and messages. Varda provides strong guarantees, enforcing the specification by static analysis, by run-time checks, and by sandboxing. To be useful, Varda takes a pragmatic approach. An OTS adaptor can contain non-Varda code (e.g., Java). Varda provides control over properties such as elasticity, placement, and inlining. Varda supports non-stop execution thanks to supervision mechanisms.